m n : (m < n) + (m = n) + (m > n). Proof. generalize (leq_dichotomy m n). snrapply (functor_sum _ idmap). snrapply equiv_leq_lt_or_eq. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids