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