We will prove mul_nat 4 2 = 8.
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 4 1 H1nat) (from left to right) at position 1.
rewrite the current goal using (mul_nat_1R 4) (from left to right) at position 1.
rewrite the current goal using add_nat_4_4_eq_8 (from left to right).
Use reflexivity.
∎