proposition: Lemma le_eq_lt x y : le x y -> (x = y) + (lt x y).
proof: Proof. induction 1. - destruct x. + left; constructor. + right; constructor. constructor. - dependent elimination IHle as [inl 1%path|inr Hlt]. + left; constructor. + right; now constructor. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded HoTT(Spaces.Nat)