We will prove mul_nat 3 3 = 9.

We prove the intermediate claim H2nat: nat_p 2.

An exact proof term for the current goal is nat_2.

We prove the intermediate claim H1nat: nat_p 1.

An exact proof term for the current goal is nat_1.

We prove the intermediate claim H3eq: 3 = ordsucc 2.

Use reflexivity.

rewrite the current goal using H3eq (from left to right) at position 1.

rewrite the current goal using (mul_nat_SR 3 2 H2nat) (from left to right) at position 1.

rewrite the current goal using H3eq (from left to right) at position 1.

rewrite the current goal using (mul_nat_SR 3 1 H1nat) (from left to right) at position 1.

rewrite the current goal using (mul_nat_1R 3) (from left to right) at position 1.

rewrite the current goal using add_nat_3_3_eq_6 (from left to right) at position 1.

rewrite the current goal using add_nat_3_6_eq_9 (from left to right) at position 1.

Use reflexivity.

∎