{n m} : ~(n < m) <-> n >= m. Proof. split. - intro; by destruct (leq_dichotomy m n). - intros ? ?; contradiction (lt_irrefl n); exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids