Let gx, rx, ux and c be given.
Assume HgxS: SNo gx.
Assume HrxS: SNo rx.
Assume HuxS: SNo ux.
Assume HcS: SNo c.
We will prove add_SNo (add_SNo gx (mul_SNo ux c)) (mul_SNo (add_SNo rx (minus_SNo ux)) c) = add_SNo gx (mul_SNo rx c).
Set uxc to be the term mul_SNo ux c.
Set rxc to be the term mul_SNo rx c.
We prove the intermediate claim HuxcS: SNo uxc.
An exact proof term for the current goal is (SNo_mul_SNo ux c HuxS HcS).
We prove the intermediate claim HrxcS: SNo rxc.
An exact proof term for the current goal is (SNo_mul_SNo rx c HrxS HcS).
We prove the intermediate claim HmUxS: SNo (minus_SNo ux).
An exact proof term for the current goal is (SNo_minus_SNo ux HuxS).
We prove the intermediate claim Hdistr: mul_SNo (add_SNo rx (minus_SNo ux)) c = add_SNo rxc (mul_SNo (minus_SNo ux) c).
We prove the intermediate claim Hdistr0: mul_SNo (add_SNo rx (minus_SNo ux)) c = add_SNo (mul_SNo rx c) (mul_SNo (minus_SNo ux) c).
An exact proof term for the current goal is (mul_SNo_distrR rx (minus_SNo ux) c HrxS HmUxS HcS).
We prove the intermediate claim HrxcDef: rxc = mul_SNo rx c.
Use reflexivity.
rewrite the current goal using HrxcDef (from left to right).
An exact proof term for the current goal is Hdistr0.
rewrite the current goal using Hdistr (from left to right).
We prove the intermediate claim HmUxC: mul_SNo (minus_SNo ux) c = minus_SNo uxc.
We prove the intermediate claim HmUxC0: mul_SNo (minus_SNo ux) c = minus_SNo (mul_SNo ux c).
An exact proof term for the current goal is (mul_SNo_minus_distrL ux c HuxS HcS).
rewrite the current goal using HmUxC0 (from left to right).
We prove the intermediate claim HuxcDef: uxc = mul_SNo ux c.
Use reflexivity.
rewrite the current goal using HuxcDef (from right to left).
Use reflexivity.
rewrite the current goal using HmUxC (from left to right).
We prove the intermediate claim HmUxcS: SNo (minus_SNo uxc).
An exact proof term for the current goal is (SNo_minus_SNo uxc HuxcS).
We prove the intermediate claim Ht2S: SNo (add_SNo rxc (minus_SNo uxc)).
An exact proof term for the current goal is (SNo_add_SNo rxc (minus_SNo uxc) HrxcS HmUxcS).
rewrite the current goal using (add_SNo_assoc gx uxc (add_SNo rxc (minus_SNo uxc)) HgxS HuxcS Ht2S) (from right to left).
rewrite the current goal using (add_SNo_assoc uxc rxc (minus_SNo uxc) HuxcS HrxcS HmUxcS) (from left to right).
rewrite the current goal using (add_SNo_com uxc rxc HuxcS HrxcS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_R2 rxc uxc HrxcS HuxcS) (from left to right) at position 1.
Use reflexivity.
∎