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

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

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

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

Use symmetry.

An exact proof term for the current goal is (add_nat_0R (n * m)).

Let k be given.

Assume Hk: nat_p k.

Assume IHk: n * (m + k) = n * m + n * k.

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

rewrite the current goal using (add_nat_SR m k Hk) (from left to right).

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

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

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

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

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

rewrite the current goal using (mul_nat_SR n k Hk) (from left to right).

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

rewrite the current goal using (add_nat_asso n Hn (n * m) (mul_nat_p n Hn m Hm) (n * k) (mul_nat_p n Hn k Hk)) (from right to left).

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

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

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

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