proposition: Lemma completeness : forall E:R -> Prop, bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
proof: Proof. intros. pose (fun x:CReal => E (Rabst x)) as Er. assert (forall x y : CReal, CRealEq x y -> Er x <-> Er y) as Erproper. { intros. unfold Er. replace (Rabst x) with (Rabst y). - reflexivity. - apply Rquot1. do 2 rewrite Rquot2. split; apply H1. } assert (exists x : CReal, Er x) as Einhab. { destruct H0. exists (Rrepr x). unfold Er. replace (Rabst (Rrepr x)) with x. - exact H0. - apply Rquot1. rewrite Rquot2. reflexivity. } assert (exists x : CReal, (forall y:CReal, Er y -> CRealLe y x)) as Ebound. { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y). apply Rrepr_le. apply H. exact Ey. } destruct (@CR_sig_lub CRealConstructive Er Erproper sig_forall_dec sig_not_dec Einhab Ebound). exists (Rabst x). split. - intros y Ey. apply Rrepr_le. rewrite Rquot2. unfold CRealLe. apply a. unfold Er. replace (Rabst (Rrepr y)) with y. + exact Ey. + apply Rquot1. rewrite Rquot2. reflexivity. - intros. destruct a. apply Rrepr_le. rewrite Rquot2. unfold CRealLe. apply H3. intros y Ey. intros. rewrite <- (Rquot2 y) in H4. apply Rrepr_le in H4. + exact H4. + apply H1, Ey. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions