proposition: Lemma le_lt_trans x y z: x ≼ y → y ≺ z → x ≺ z.
proof: Proof. rewrite !lt_spec. intros leyz [lexy ngexy]; split; [|contradict ngexy]; etransitivity; eassumption. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)