Let n be given.

Assume Hn.

Let m be given.

Assume Hm.

Let k be given.

Assume Hk: k ∈ m.

We will prove n + k ∈ n + m.

rewrite the current goal using add_nat_com n Hn k (nat_p_trans m Hm k Hk) (from left to right).

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

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

∎