Apply nat_ind to the current goal.
We will prove ∀m ∈ 0, m ⊆ 0.
Let m be given.
Assume Hm: m ∈ 0.
We will prove False.
An exact proof term for the current goal is (EmptyE m Hm).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: ∀m ∈ n, m ⊆ n.
We will prove ∀m ∈ ordsucc n, m ⊆ ordsucc n.
Let m be given.
Assume Hm: m ∈ ordsucc n.
Apply (ordsuccE n m Hm) to the current goal.
Assume H1: m ∈ n.
We will prove m ⊆ ordsucc n.
Apply (Subq_tra m n (ordsucc n)) to the current goal.
An exact proof term for the current goal is (IHn m H1).
An exact proof term for the current goal is (ordsuccI1 n).
Assume H1: m = n.
We will prove m ⊆ ordsucc n.
rewrite the current goal using H1 (from left to right).
We will prove n ⊆ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n).
∎