We prove the intermediate
claim H0nat:
nat_p 0.
An
exact proof term for the current goal is
nat_0.
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 H2nat:
nat_p 2.
An
exact proof term for the current goal is
nat_2.
We prove the intermediate
claim H3eq:
3 = ordsucc 2.
rewrite the current goal using H3eq (from left to right) at position 1.
rewrite the current goal using
(add_nat_SR 3 2 H2nat) (from left to right) at position 1.
rewrite the current goal using
(add_nat_SR 3 1 H1nat) (from left to right) at position 1.
rewrite the current goal using
(add_nat_SR 3 0 H0nat) (from left to right) at position 1.
rewrite the current goal using
(add_nat_0R 3) (from left to right) at position 1.
Use reflexivity.
∎