Let k be given.

Assume Hk: nat_p k.

Let m be given.

Assume Hm: nat_p m.

Assume Hkm: k ⊆ m.

Let n be given.

Assume Hn: nat_p n.

Apply ordinal_In_Or_Subq k m (nat_p_ordinal k Hk) (nat_p_ordinal m Hm) to the current goal.

Assume H1: k ∈ m.

We will prove k + n ⊆ m + n.

Apply nat_trans (m + n) (add_nat_p m Hm n Hn) to the current goal.

We will prove k + n ∈ m + n.

An exact proof term for the current goal is add_nat_In_R m Hm k H1 n Hn.

Assume H1: m ⊆ k.

We prove the intermediate claim L1: k = m.

Apply set_ext to the current goal.

An exact proof term for the current goal is Hkm.

An exact proof term for the current goal is H1.

We will prove k + n ⊆ m + n.

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

Apply Subq_ref to the current goal.

∎