We will prove add_nat 3 6 = 9.

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 H4nat: nat_p 4.

An exact proof term for the current goal is (nat_ordsucc 3 H3nat).

We prove the intermediate claim H5nat: nat_p 5.

An exact proof term for the current goal is (nat_ordsucc 4 H4nat).

We prove the intermediate claim H6eq: 6 = ordsucc 5.

Use reflexivity.

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

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

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

rewrite the current goal using (add_nat_SR 3 3 H3nat) (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.

∎