Let x, y and z be given.
Assume Hx Hx0 Hy Hz.
Assume H1: x * y = x * z.
We will prove y = z.
rewrite the current goal using mul_SNo_oneL y Hy (from right to left).
rewrite the current goal using mul_SNo_oneL z Hz (from right to left).
We will prove 1 * y = 1 * z.
rewrite the current goal using recip_SNo_invL x Hx Hx0 (from right to left).
We will prove (recip_SNo x * x) * y = (recip_SNo x * x) * z.
rewrite the current goal using mul_SNo_assoc (recip_SNo x) x y (SNo_recip_SNo x Hx) Hx Hy (from right to left).
rewrite the current goal using mul_SNo_assoc (recip_SNo x) x z (SNo_recip_SNo x Hx) Hx Hz (from right to left).
We will prove recip_SNo x * (x * y) = recip_SNo x * (x * z).
Use f_equal.
An exact proof term for the current goal is H1.
∎