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.