We will prove m ⊆ m + 0.

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

Apply Subq_ref to the current goal.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: m ⊆ m + n.

We will prove m ⊆ m + ordsucc n.

rewrite the current goal using add_nat_SR m n Hn (from left to right).

We will prove m ⊆ ordsucc (m + n).

Apply Subq_tra m (m + n) (ordsucc (m + n)) IHn to the current goal.

We will prove m + n ⊆ ordsucc (m + n).

Apply ordsuccI1 to the current goal.