Let x be given.
Assume HxS: SNo x.
Assume H0ltx: 0 < x.
Assume H1lex: 1 ≤ x.
Set r to be the term recip_SNo_pos x.
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (SNo_recip_SNo_pos x HxS H0ltx).
We prove the intermediate claim Hrpos: 0 < r.
An exact proof term for the current goal is (recip_SNo_pos_is_pos x HxS H0ltx).
We prove the intermediate claim HrNN: 0 ≤ r.
An exact proof term for the current goal is (SNoLtLe 0 r Hrpos).
We prove the intermediate claim Hxrx: mul_SNo x r = 1.
An exact proof term for the current goal is (recip_SNo_pos_invR x HxS H0ltx).
We prove the intermediate claim Hrx: mul_SNo r x = 1.
We prove the intermediate claim Hcomm: mul_SNo x r = mul_SNo r x.
An exact proof term for the current goal is (mul_SNo_com x r HxS HrS).
rewrite the current goal using Hcomm (from right to left).
An exact proof term for the current goal is Hxrx.
We prove the intermediate claim Hrle: mul_SNo r 1 ≤ mul_SNo r x.
An exact proof term for the current goal is (nonneg_mul_SNo_Le r 1 x HrS HrNN SNo_1 HxS H1lex).
rewrite the current goal using (mul_SNo_oneR r HrS) (from right to left) at position 1.
rewrite the current goal using Hrx (from right to left) at position 2.
An exact proof term for the current goal is Hrle.
∎