proposition: Lemma common_wo S (Sc: common S): well_ordered S.
proof: Proof. destruct Sc as [[sub _] _], Cg as [[total wo] _]. clear -sub total wo. split; firstorder. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)