Let n be given.

Assume Hn: nat_p n.

Let m be given.

Assume Hm: m ∈ ordsucc n.

Let k be given.

Assume Hk: k ∈ m.

We will prove k ∈ n.

Apply (ordsuccE n m Hm) to the current goal.

Assume H1: m ∈ n.

An exact proof term for the current goal is nat_trans n Hn m H1 k Hk.

Assume H1: m = n.

rewrite the current goal using H1 (from right to left).

An exact proof term for the current goal is Hk.

∎