Let n be given.
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.
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.
rewrite the current goal using
mul_SNo_zeroR n Ln3 (from left to right).
An
exact proof term for the current goal is
mul_nat_0R n.
Let m be given.
An
exact proof term for the current goal is
mul_nat_SR n m Hm.
Use f_equal.
An exact proof term for the current goal is IH.
Use symmetry.
We will
prove n * (1 + m) = n + n * m.
We will
prove n * 1 + n * m = n + n * m.
Use f_equal.
An
exact proof term for the current goal is
mul_SNo_oneR n Ln3.
Let m be given.
An
exact proof term for the current goal is
L1 m (omega_nat_p m Hm).
∎