proposition: Lemma wo_lt_ge X (Xwo: well_ordered X) x y (inx: x ∈ X) (iny: y ∈ X): x ≺ y ∨ y ≼ x.
proof: Proof. destruct (classic (y ≼ x)); auto. destruct (wo_total X Xwo x y); auto. rewrite ltA_spec; auto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)