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