{n m} k : n <= m + k -> n - k <= m. Proof. intros H. apply (nat_sub_monotone_l k) in H. by rewrite nat_add_sub_cancel_r in H. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids