proposition: Lemma common_comparable S S' (Sc: common S) (Sc': common S'): S ≼ S' ∨ S' ≼ S.
proof: Proof. destruct Sc as [subc _], Sc' as [subc' _]. destruct (classic (C ≼ S)) as [leC|ltS]; [right; etransitivity; eauto|]. destruct (classic (C ≼ S')) as [leC|ltS']; [left; etransitivity; eauto|]. destruct (initial_prefix C S) as [x [inx [notinx prefix]]]; [auto using C_wo|split; auto|]. destruct (initial_prefix C S') as [x' [inx' [notinx' prefix']]]; [auto using C_wo|split; auto|]. rewrite prefix, prefix'. now destruct (wo_total C (C_wo _ Cg) x x' inx inx') as [case|case]; [left|right]; apply restrict_mono. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)