{n m} k : m <= k -> n <= k -> k - n <= k - m -> m <= n. Proof. intros H1 H2 H3. apply (nat_sub_monotone_r k) in H3. rewrite 2 nat_sub_sub_cancel_r in H3; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids