{n m} k : n - k <= m -> n <= k + m. Proof. intros H. rewrite nat_add_comm. apply (nat_add_r_monotone k) in H. rapply leq_trans. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids