Apply nat_complete_ind to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ∀m ∈ n, ⋃ (ordsucc m) = m.

We will prove ⋃ (ordsucc n) = n.

Apply set_ext to the current goal.

Let m be given.

Assume Hm: m ∈ ⋃ (ordsucc n).

Apply (UnionE_impred (ordsucc n) m Hm) to the current goal.

Let k be given.

Assume H1: m ∈ k.

Assume H2: k ∈ ordsucc n.

We will prove m ∈ n.

An exact proof term for the current goal is nat_ordsucc_trans n Hn k H2 m H1.

Let m be given.

Assume Hm: m ∈ n.

We will prove m ∈ ⋃ (ordsucc n).

Apply (UnionI (ordsucc n) m n) to the current goal.

An exact proof term for the current goal is Hm.

An exact proof term for the current goal is (ordsuccI2 n).

∎