proposition: Lemma W_wo: well_ordered W.
proof: Proof. apply union_wo; auto using common_wo, common_comparable. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)