{n m} k : k <= m -> n <= m - k -> k + n <= m. Proof. intros H1 H2. rapply (leq_reflects_sub_l k). by rewrite nat_add_sub_cancel_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids