Let a, b, c and d be given.
Assume HaS: SNo a.
Assume HbS: SNo b.
Assume HcS: SNo c.
Assume HdS: SNo d.
Set ac to be the term mul_SNo a c.
Set bd to be the term mul_SNo b d.
Set ad to be the term mul_SNo a d.
Set bc to be the term mul_SNo b c.
Set lhs to be the term mul_SNo (add_SNo ac bd) (add_SNo ac bd).
Set rhs to be the term mul_SNo (add_SNo (mul_SNo a a) (mul_SNo b b)) (add_SNo (mul_SNo c c) (mul_SNo d d)).
Set diff to be the term add_SNo ad (minus_SNo bc).
Set diff2 to be the term mul_SNo diff diff.
We prove the intermediate claim HacS: SNo ac.
An exact proof term for the current goal is (SNo_mul_SNo a c HaS HcS).
We prove the intermediate claim HbdS: SNo bd.
An exact proof term for the current goal is (SNo_mul_SNo b d HbS HdS).
We prove the intermediate claim HadS: SNo ad.
An exact proof term for the current goal is (SNo_mul_SNo a d HaS HdS).
We prove the intermediate claim HbcS: SNo bc.
An exact proof term for the current goal is (SNo_mul_SNo b c HbS HcS).
We prove the intermediate claim HdiffS: SNo diff.
An exact proof term for the current goal is (SNo_add_SNo ad (minus_SNo bc) HadS (SNo_minus_SNo bc HbcS)).
We prove the intermediate claim Hdiff2S: SNo diff2.
An exact proof term for the current goal is (SNo_mul_SNo diff diff HdiffS HdiffS).
We prove the intermediate claim Hdiff2NN: 0 ≤ diff2.
An exact proof term for the current goal is (SNo_sqr_nonneg diff HdiffS).
We prove the intermediate claim Hrhs_eq: rhs = add_SNo lhs diff2.
We prove the intermediate claim HaaS: SNo (mul_SNo a a).
An exact proof term for the current goal is (SNo_mul_SNo a a HaS HaS).
We prove the intermediate claim HbbS: SNo (mul_SNo b b).
An exact proof term for the current goal is (SNo_mul_SNo b b HbS HbS).
We prove the intermediate claim HccS: SNo (mul_SNo c c).
An exact proof term for the current goal is (SNo_mul_SNo c c HcS HcS).
We prove the intermediate claim HddS: SNo (mul_SNo d d).
An exact proof term for the current goal is (SNo_mul_SNo d d HdS HdS).
We prove the intermediate claim HlhsDef: lhs = mul_SNo (add_SNo ac bd) (add_SNo ac bd).
Use reflexivity.
We prove the intermediate claim HdiffDef: diff = add_SNo ad (minus_SNo bc).
Use reflexivity.
We prove the intermediate claim Hdiff2Def: diff2 = mul_SNo diff diff.
Use reflexivity.
rewrite the current goal using HlhsDef (from left to right).
rewrite the current goal using Hdiff2Def (from left to right).
rewrite the current goal using HdiffDef (from left to right).
rewrite the current goal using (SNo_foil (mul_SNo a a) (mul_SNo b b) (mul_SNo c c) (mul_SNo d d) HaaS HbbS HccS HddS) (from left to right).
rewrite the current goal using (SNo_foil ac bd ac bd HacS HbdS HacS HbdS) (from left to right).
rewrite the current goal using (SNo_foil_mm ad bc ad bc HadS HbcS HadS HbcS) (from left to right).
We prove the intermediate claim HabS: SNo (mul_SNo a b).
An exact proof term for the current goal is (SNo_mul_SNo a b HaS HbS).
We prove the intermediate claim HcdS: SNo (mul_SNo c d).
An exact proof term for the current goal is (SNo_mul_SNo c d HcS HdS).
We prove the intermediate claim HdcS: SNo (mul_SNo d c).
An exact proof term for the current goal is (SNo_mul_SNo d c HdS HcS).
We prove the intermediate claim Hdc_eq_cd: mul_SNo d c = mul_SNo c d.
An exact proof term for the current goal is (mul_SNo_com d c HdS HcS).
We prove the intermediate claim Hadbc_eq_acbd: mul_SNo ad bc = mul_SNo ac bd.
We prove the intermediate claim HadDef: ad = mul_SNo a d.
Use reflexivity.
We prove the intermediate claim HbcDef: bc = mul_SNo b c.
Use reflexivity.
We prove the intermediate claim HacDef: ac = mul_SNo a c.
Use reflexivity.
We prove the intermediate claim HbdDef: bd = mul_SNo b d.
Use reflexivity.
rewrite the current goal using HadDef (from left to right).
rewrite the current goal using HbcDef (from left to right).
rewrite the current goal using HacDef (from left to right).
rewrite the current goal using HbdDef (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid a d b c HaS HdS HbS HcS) (from left to right).
rewrite the current goal using Hdc_eq_cd (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid a c b d HaS HcS HbS HdS) (from right to left).
Use reflexivity.
We prove the intermediate claim Hbcad_eq_bdac: mul_SNo bc ad = mul_SNo bd ac.
We prove the intermediate claim HadDef: ad = mul_SNo a d.
Use reflexivity.
We prove the intermediate claim HbcDef: bc = mul_SNo b c.
Use reflexivity.
We prove the intermediate claim HacDef: ac = mul_SNo a c.
Use reflexivity.
We prove the intermediate claim HbdDef: bd = mul_SNo b d.
Use reflexivity.
rewrite the current goal using HadDef (from left to right).
rewrite the current goal using HbcDef (from left to right).
rewrite the current goal using HacDef (from left to right).
rewrite the current goal using HbdDef (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid b c a d HbS HcS HaS HdS) (from left to right).
rewrite the current goal using Hdc_eq_cd (from right to left).
rewrite the current goal using (mul_SNo_com_4_inner_mid b d a c HbS HdS HaS HcS) (from right to left).
Use reflexivity.
rewrite the current goal using Hadbc_eq_acbd (from left to right).
rewrite the current goal using Hbcad_eq_bdac (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid a a c c HaS HaS HcS HcS) (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid a a d d HaS HaS HdS HdS) (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid b b c c HbS HbS HcS HcS) (from left to right).
rewrite the current goal using (mul_SNo_com_4_inner_mid b b d d HbS HbS HdS HdS) (from left to right).
We prove the intermediate claim HacacS2: SNo (mul_SNo ac ac).
An exact proof term for the current goal is (SNo_mul_SNo ac ac HacS HacS).
We prove the intermediate claim HadadS2: SNo (mul_SNo ad ad).
An exact proof term for the current goal is (SNo_mul_SNo ad ad HadS HadS).
We prove the intermediate claim HbcbcS2: SNo (mul_SNo bc bc).
An exact proof term for the current goal is (SNo_mul_SNo bc bc HbcS HbcS).
We prove the intermediate claim HbdbdS2: SNo (mul_SNo bd bd).
An exact proof term for the current goal is (SNo_mul_SNo bd bd HbdS HbdS).
We prove the intermediate claim HacbdS2: SNo (mul_SNo ac bd).
An exact proof term for the current goal is (SNo_mul_SNo ac bd HacS HbdS).
We prove the intermediate claim HbdacS2: SNo (mul_SNo bd ac).
An exact proof term for the current goal is (SNo_mul_SNo bd ac HbdS HacS).
We prove the intermediate claim HmacbdS2: SNo (minus_SNo (mul_SNo ac bd)).
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo ac bd) HacbdS2).
We prove the intermediate claim HmbdacS2: SNo (minus_SNo (mul_SNo bd ac)).
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo bd ac) HbdacS2).
We prove the intermediate claim Hbdac_bdbdS: SNo (add_SNo (mul_SNo bd ac) (mul_SNo bd bd)).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo bd ac) (mul_SNo bd bd) HbdacS2 HbdbdS2).
We prove the intermediate claim Hmbdac_bcbcS: SNo (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)).
An exact proof term for the current goal is (SNo_add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc) HmbdacS2 HbcbcS2).
rewrite the current goal using (add_SNo_com (mul_SNo ac bd) (add_SNo (mul_SNo bd ac) (mul_SNo bd bd)) HacbdS2 Hbdac_bdbdS) (from left to right).
rewrite the current goal using (add_SNo_assoc (mul_SNo ac ac) (add_SNo (mul_SNo bd ac) (mul_SNo bd bd)) (mul_SNo ac bd) HacacS2 Hbdac_bdbdS HacbdS2) (from left to right).
We prove the intermediate claim HinnerR1S: SNo (add_SNo (minus_SNo (mul_SNo ac bd)) (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc))).
An exact proof term for the current goal is (SNo_add_SNo (minus_SNo (mul_SNo ac bd)) (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)) HmacbdS2 Hmbdac_bcbcS).
rewrite the current goal using (add_SNo_com (mul_SNo ad ad) (add_SNo (minus_SNo (mul_SNo ac bd)) (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc))) HadadS2 HinnerR1S) (from left to right).
rewrite the current goal using (add_SNo_assoc (minus_SNo (mul_SNo ac bd)) (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)) (mul_SNo ad ad) HmacbdS2 Hmbdac_bcbcS HadadS2) (from right to left).
We prove the intermediate claim Hw1S: SNo (add_SNo (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)) (mul_SNo ad ad)).
An exact proof term for the current goal is (SNo_add_SNo (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)) (mul_SNo ad ad) Hmbdac_bcbcS HadadS2).
rewrite the current goal using (add_SNo_assoc (mul_SNo ac ac) (add_SNo (mul_SNo bd ac) (mul_SNo bd bd)) (mul_SNo ac bd) HacacS2 Hbdac_bdbdS HacbdS2) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_prop3 (mul_SNo ac ac) (add_SNo (mul_SNo bd ac) (mul_SNo bd bd)) (mul_SNo ac bd) (add_SNo (add_SNo (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc)) (mul_SNo ad ad)) HacacS2 Hbdac_bdbdS HacbdS2 Hw1S) (from left to right).
We prove the intermediate claim Hbcbc_adadS: SNo (add_SNo (mul_SNo bc bc) (mul_SNo ad ad)).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo bc bc) (mul_SNo ad ad) HbcbcS2 HadadS2).
rewrite the current goal using (add_SNo_assoc (minus_SNo (mul_SNo bd ac)) (mul_SNo bc bc) (mul_SNo ad ad) HmbdacS2 HbcbcS2 HadadS2) (from right to left).
rewrite the current goal using (add_SNo_com_4_inner_mid (mul_SNo bd ac) (mul_SNo bd bd) (minus_SNo (mul_SNo bd ac)) (add_SNo (mul_SNo bc bc) (mul_SNo ad ad)) HbdacS2 HbdbdS2 HmbdacS2 Hbcbc_adadS) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv (mul_SNo bd ac) HbdacS2) (from left to right).
rewrite the current goal using (add_SNo_0L (add_SNo (mul_SNo bd bd) (add_SNo (mul_SNo bc bc) (mul_SNo ad ad))) (SNo_add_SNo (mul_SNo bd bd) (add_SNo (mul_SNo bc bc) (mul_SNo ad ad)) HbdbdS2 Hbcbc_adadS)) (from left to right).
rewrite the current goal using (add_SNo_com (mul_SNo bc bc) (mul_SNo ad ad) HbcbcS2 HadadS2) (from left to right).
We prove the intermediate claim Hadad_bcbcS: SNo (add_SNo (mul_SNo ad ad) (mul_SNo bc bc)).
An exact proof term for the current goal is (SNo_add_SNo (mul_SNo ad ad) (mul_SNo bc bc) HadadS2 HbcbcS2).
rewrite the current goal using (add_SNo_com (mul_SNo bd bd) (add_SNo (mul_SNo ad ad) (mul_SNo bc bc)) HbdbdS2 Hadad_bcbcS) (from left to right).
rewrite the current goal using (add_SNo_assoc (mul_SNo ad ad) (mul_SNo bc bc) (mul_SNo bd bd) HadadS2 HbcbcS2 HbdbdS2) (from right to left).
Use reflexivity.
rewrite the current goal using Hrhs_eq (from left to right).
We prove the intermediate claim HlhsS: SNo lhs.
An exact proof term for the current goal is (SNo_mul_SNo (add_SNo ac bd) (add_SNo ac bd) (SNo_add_SNo ac bd HacS HbdS) (SNo_add_SNo ac bd HacS HbdS)).
An exact proof term for the current goal is (SNoLe_add_nonneg_right lhs diff2 HlhsS Hdiff2S Hdiff2NN).
∎