proposition: Corollary gsets_inconsistent: False.
proof: Proof. destruct (domain maxgset (C_wo _ maxgset_gset)) as [b b_bound]. enough (b ∈ maxgset) as contra. - eapply upper_bound in contra; eauto using C_wo, maxgset_gset. now apply irreflexivity in contra. - eapply prefix_union; eauto using gsets_comparable, maxgset_suspend. now right. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)