proposition: Lemma maxgset_gset: gset maxgset.
proof: Proof. split. - apply union_wo. + apply gsets_comparable. + destruct 1; trivial. - intros c [S [inS inc]]. enough (restrict c maxgset ≌ restrict c S) as -> by now apply C_bounds. apply subset_equ. + intros x [[S' [inS' sub]] ltc]. split; trivial. destruct (gsets_comparable S S') as [case|case]; auto. * eapply cs_closed; eauto. apply ltA_spec, ltc. * eapply cs_subset; eauto. + intros x [inx ltc]; split; trivial. exists S; auto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)