{n m} k : n <= m -> k - m <= k - n. Proof. intros H. induction k. - by rewrite nat_sub_zero_l. - destruct (leq_dichotomy m k) as [l|r]. + rewrite 2 nat_sub_succ_l; exact _. + apply equiv_nat_sub_leq in r. destruct r^. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids