proposition: Corollary must_have_included_bound (g: set → A → Prop) (unique: ∀ S b b', g S b → g S b' → b ≌ b') (proper: Proper (equ ==> equ ==> iff) g) (domain: ∀ S, well_ordered S → ∃ b, g S b) (upper_bound: ∀ S b x, well_ordered S → g S b → x ∈ S → x ≼ b) (strong_upper_bounds: ∀ S b, well_ordered S → g S b → (∃ b', ∀ x, x ∈ S → x ≺ b') → ¬b ∈ S): ∃ S b, well_ordered S ∧ g S b ∧ b ∈ S.
proof: Proof. destruct (classic (∃ S b, well_ordered S ∧ g S b ∧ b ∈ S)) as [|contra]; trivial. destruct (gsets_inconsistent g unique proper domain). intros * woS b_bound inx. apply ltA_spec. split; [eapply upper_bound; eauto|]. intro leb. assert (b ≌ x) as eqb. { apply eqA_spec; split; trivial. eapply upper_bound; eauto. } rewrite eqb in *; clear b eqb. eapply strong_upper_bounds in inx; eauto. destruct (classic (∃ b', ∀ y, y ∈ S → y ≺ b')) as [|contra']; trivial. contradict contra. exists S, x. repeat (split; trivial). Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)