{n m} k : k <= n -> n < k + m -> n - k < m. Proof. intros H1 H2; unfold lt. rewrite <- nat_sub_succ_l; only 2: exact _. rewrite <- (nat_add_sub_cancel_l m k). by apply nat_sub_monotone_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids