We will prove 0 * 0 = 0.

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

Let m be given.

Assume Hm: nat_p m.

Assume IHm: 0 * m = 0.

We will prove 0 * ordsucc m = 0.

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

We will prove 0 + 0 * m = 0.

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

We will prove 0 + 0 = 0.

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