Let n be given.

Assume Hn: nat_p n.

Let k be given.

Assume Hk: nat_p k.

Let m be given.

Assume Hm: nat_p m.

Assume Hkm: k ⊆ m.

rewrite the current goal using add_nat_com n Hn 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_Subq_R k Hk m Hm Hkm n Hn.

∎