We will prove add_nat 4 4 = 8.

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 H3nat: nat_p 3.

An exact proof term for the current goal is (nat_ordsucc 2 nat_2).

We prove the intermediate claim H4eq: 4 = ordsucc 3.

Use reflexivity.

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

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

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

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

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

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

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

Use reflexivity.

∎