We will prove mul_nat 2 2 = 4.

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 H2eq: 2 = ordsucc 1.

Use reflexivity.

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

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

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

rewrite the current goal using H2eq (from left to right) at position 2.

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

We prove the intermediate claim H1eq: 1 = ordsucc 0.

Use reflexivity.

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

rewrite the current goal using (add_nat_SR 2 0 nat_0) (from left to right) at position 1.

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

Use reflexivity.

∎