We will prove ordsucc n * 0 = n * 0 + 0.

rewrite the current goal using mul_nat_0R (from left to right).

We will prove 0 = 0 + 0.

Use symmetry.

An exact proof term for the current goal is (add_nat_0R 0).

Let m be given.

Assume Hm: nat_p m.

Assume IHm: ordsucc n * m = n * m + m.

rewrite the current goal using (mul_nat_SR (ordsucc n) m Hm) (from left to right).

We will prove ordsucc n + ordsucc n * m = n * ordsucc m + ordsucc m.

rewrite the current goal using IHm (from left to right).

We will prove ordsucc n + (n * m + m) = n * ordsucc m + ordsucc m.

rewrite the current goal using add_nat_SL (from left to right).

We will prove ordsucc (n + (n * m + m)) = n * ordsucc m + ordsucc m.

rewrite the current goal using (mul_nat_SR n m Hm) (from left to right).

We will prove ordsucc (n + (n * m + m)) = (n + n * m) + ordsucc m.

rewrite the current goal using (add_nat_SR (n + n * m) m Hm) (from left to right).

We will prove ordsucc (n + (n * m + m)) = ordsucc ((n + n * m) + m).

rewrite the current goal using add_nat_asso (from left to right).

Use reflexivity.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is (mul_nat_p n Hn m Hm).

An exact proof term for the current goal is Hm.

An exact proof term for the current goal is Hn.

An exact proof term for the current goal is (add_nat_p (n * m) (mul_nat_p n Hn m Hm) m Hm).