Apply nat_inv_impred to the current goal.

Apply orIL to the current goal.

Use reflexivity.

Let n be given.

Assume Hn.

Apply orIR to the current goal.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hn.

Use reflexivity.

∎