proposition: Lemma gsets_comparable C D (Cg: gset C) (Dg: gset D): C ≼ D ∨ D ≼ C.
proof: Proof. pose proof (W_le_C C D) as leC. pose proof (W_le_D C D) as leD. assert (W C D ≌ C ∨ W C D ≺ C) as [<-|ltC]; auto. { unfold lt, set_lt, default_lt, equ, set_eq, default_eq. destruct (classic (C ≼ W C D)); auto. } assert (W C D ≌ D ∨ W C D ≺ D) as [<-|ltD]; auto. { unfold lt, set_lt, default_lt, equ, set_eq, default_eq. destruct (classic (D ≼ W C D)); auto. } clear leC leD. destruct (initial_prefix C (W C D)) as [c [inc [notinc eqc]]]; auto using C_wo. destruct (initial_prefix D (W C D)) as [d [ind [notind eqd]]]; auto using C_wo. destruct (incomparable_C_D_inconsistent C D Cg Dg c d eqc eqd inc ind). Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)