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