Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Ln1: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Ln2: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Ln1.
We prove the intermediate claim Ln3: SNo n.
An exact proof term for the current goal is ordinal_SNo n Ln2.
We prove the intermediate claim L1: ∀m, nat_p m → mul_nat n m = n * m.
Apply nat_ind to the current goal.
We will prove mul_nat n 0 = n * 0.
rewrite the current goal using mul_SNo_zeroR n Ln3 (from left to right).
We will prove mul_nat n 0 = 0.
An exact proof term for the current goal is mul_nat_0R n.
Let m be given.
Assume Hm: nat_p m.
Assume IH: mul_nat n m = n * m.
We will prove mul_nat n (ordsucc m) = n * (ordsucc m).
Use transitivity with add_nat n (mul_nat n m), n + (mul_nat n m), and n + (n * m).
An exact proof term for the current goal is mul_nat_SR n m Hm.
An exact proof term for the current goal is add_nat_add_SNo n Hn (mul_nat n m) (nat_p_omega (mul_nat n m) (mul_nat_p n Ln1 m Hm)).
Use f_equal.
An exact proof term for the current goal is IH.
We will prove n + n * m = n * ordsucc m.
Use symmetry.
We will prove n * ordsucc m = n + n * m.
rewrite the current goal using add_SNo_0L m (ordinal_SNo m (nat_p_ordinal m Hm)) (from right to left) at position 1.
We will prove n * ordsucc (0 + m) = n + n * m.
rewrite the current goal using add_SNo_ordinal_SL 0 ordinal_Empty m (nat_p_ordinal m Hm) (from right to left).
We will prove n * (1 + m) = n + n * m.
rewrite the current goal using mul_SNo_distrL n 1 m Ln3 SNo_1 (ordinal_SNo m (nat_p_ordinal m Hm)) (from left to right).
We will prove n * 1 + n * m = n + n * m.
Use f_equal.
We will prove n * 1 = n.
An exact proof term for the current goal is mul_SNo_oneR n Ln3.
Let m be given.
Assume Hm: m ∈ ω.
We will prove mul_nat n m = n * m.
An exact proof term for the current goal is L1 m (omega_nat_p m Hm).
∎