{n m} k : k <= m -> n - k <= m - k -> n <= m. Proof. intros ineq1 ineq2. apply (nat_add_r_monotone k) in ineq2. apply (@leq_trans _ (n - k + k) _ (leq_sub_add_l _ _)). apply (@leq_trans _ (m - k + k) _ _). by rewrite nat_add_sub_l_cancel. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids