We will prove n * 0 = 0 * n.

rewrite the current goal using (mul_nat_0L n Hn) (from left to right).

An exact proof term for the current goal is (mul_nat_0R n).

Let m be given.

Assume Hm: nat_p m.

Assume IHm: n * m = m * n.

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

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

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

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

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

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

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

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