proposition: Lemma glb_dec_Q : forall {R : ConstructiveReals} (upcut : DedekindDecCut), { x : CRcarrier R | forall r:Q, (x < CR_of_Q R r -> DDupcut upcut r) /\ (CR_of_Q R r < x -> ~DDupcut upcut r) }.
proof: Proof. intros. assert (forall a b : Q, Qle a b -> Qle (-b) (-a)). { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. } assert (CR_cauchy R (fun n:nat => CR_of_Q R (proj1_sig (DDcut_limit upcut (1#Pos.of_nat n) (eq_refl _))))). { intros p. exists (Pos.to_nat p). intros i j pi pj. destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl), (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig. apply (CRabs_le). split. - intros. unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_le. apply (Qplus_le_l _ _ x0). ring_simplify. setoid_replace (-1 * (1 # p) + x0)%Q with (x0 - (1 # p))%Q. 2: ring. apply (Qle_trans _ (x0- (1#Pos.of_nat j))). + apply Qplus_le_r. apply H. apply Z2Nat.inj_le. * discriminate. * discriminate. * simpl. rewrite Nat2Pos.id. -- exact pj. -- intro abs. subst j. inversion pj. pose proof (Pos2Nat.is_pos p). rewrite H1 in H0. inversion H0. + apply Qlt_le_weak, (DDlow_below_up upcut). * apply a. * apply a0. - unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus. apply CR_of_Q_le. apply (Qplus_le_l _ _ (x0-(1#p))). ring_simplify. setoid_replace (x -1 * (1 # p))%Q with (x - (1 # p))%Q. 2: ring. apply (Qle_trans _ (x- (1#Pos.of_nat i))). + apply Qplus_le_r. apply H. apply Z2Nat.inj_le. * discriminate. * discriminate. * simpl. rewrite Nat2Pos.id. -- exact pi. -- intro abs. subst i. inversion pi. pose proof (Pos2Nat.is_pos p). rewrite H1 in H0. inversion H0. + apply Qlt_le_weak, (DDlow_below_up upcut). * apply a0. * apply a. } apply CR_complete in H0. destruct H0 as [l lcv]. exists l. split. - intros. destruct (CR_cv_open_above _ (CR_of_Q R r) l lcv H0) as [p pmaj]. specialize (pmaj p (Nat.le_refl p)). unfold proj1_sig in pmaj. destruct (DDcut_limit upcut (1 # Pos.of_nat p) eq_refl) as [q qmaj]. apply (DDinterval upcut q). 2: apply qmaj. destruct (Q_dec q r). + destruct s. * apply Qlt_le_weak, q0. * exfalso. apply (CR_of_Q_lt R) in q0. exact (CRlt_asym _ _ pmaj q0). + rewrite q0. apply Qle_refl. - intros H0 abs. assert ((CR_of_Q R r+l) * CR_of_Q R (1#2) < l). { apply (CRmult_lt_reg_r (CR_of_Q R 2)). - apply CR_of_Q_pos. reflexivity. - rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. apply CRplus_lt_compat_r. exact H0. } destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj]. assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)). { apply CRmult_lt_0_compat. - rewrite <- (CRplus_opp_r (CR_of_Q R r)). apply CRplus_lt_compat_r. exact H0. - apply CR_of_Q_pos. reflexivity. } destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj]. destruct i. + exfalso. simpl in imaj. exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)). + specialize (pmaj (max (S i) (S p)) (Nat.le_trans p (S p) _ (le_S p p (Nat.le_refl p)) (Nat.le_max_r (S i) (S p)))). unfold proj1_sig in pmaj. destruct (DDcut_limit upcut (1 # Pos.of_nat (max (S i) (S p))) eq_refl) as [q qmaj]. destruct qmaj. apply H4. clear H4. apply (DDinterval upcut r). 2: exact abs. apply (Qplus_le_l _ _ (1 # Pos.of_nat (Init.Nat.max (S i) (S p)))). ring_simplify. apply (Qle_trans _ (r + (1 # Pos.of_nat (S i)))). * rewrite Qplus_le_r. unfold Qle,Qnum,Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id. -- apply Nat.le_max_l. -- discriminate. -- discriminate. * apply (CRmult_lt_compat_l ((l - CR_of_Q R r) * CR_of_Q R (1 # 2))) in imaj. 2: exact H2. rewrite CRinv_r in imaj. destruct (Q_dec (r+(1#Pos.of_nat (S i))) q);[|rewrite q0; apply Qle_refl]. destruct s. { apply Qlt_le_weak, q0. } exfalso. apply (CR_of_Q_lt R) in q0. apply (CRlt_asym _ _ pmaj). apply (CRlt_le_trans _ _ _ q0). apply (CRplus_le_reg_l (-CR_of_Q R r)). rewrite CR_of_Q_plus, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply (CRmult_lt_compat_r (CR_of_Q R (1 # Pos.of_nat (S i)))) in imaj. -- rewrite CRmult_1_l in imaj. apply (CRle_trans _ ( (l - CR_of_Q R r) * CR_of_Q R (1 # 2) * CR_of_Q R (Z.of_nat (S i) # 1) * CR_of_Q R (1 # Pos.of_nat (S i)))). ++ apply CRlt_asym, imaj. ++ rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q. ** rewrite CRmult_1_r. unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)). rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r. rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite <- CR_of_Q_mult, <- CR_of_Q_opp, <- CR_of_Q_mult, <- CR_of_Q_plus. apply CR_of_Q_le. ring_simplify. apply Qle_refl. ** unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. rewrite Z.mul_1_l, Pos.mul_1_l. unfold Z.of_nat. apply f_equal. apply Pos.of_nat_succ. -- apply CR_of_Q_pos. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveAbs ConstructiveLimits Logic.ConstructiveEpsilon