proposition: Lemma DRealOpen : forall (x : DReal) (q : Q), proj1_sig x q = true -> { r : Q | Qlt q r /\ proj1_sig x r = true }.
proof: Proof. intros. destruct (sig_forall_dec (fun n => Qle (proj1_sig (DRealQlim x n)) q)). - intro n. destruct (DRealQlim x n); unfold proj1_sig. destruct (Qlt_le_dec q x0). + right. exact (Qlt_not_le _ _ q0). + left. exact q0. - destruct s. apply Qnot_le_lt in n. destruct (DRealQlim x x0); unfold proj1_sig in n. exists x1. split. + exact n. + apply a. - exfalso. destruct x as [f low]. unfold proj1_sig in H, q0. destruct low, a, a. apply (n1 q H). intros. destruct (Qlt_le_dec q r). 2: left; exact q1. right. destruct (Qarchimedean (/(r - q))) as [p pmaj]. specialize (q0 (Pos.to_nat p)). destruct (DRealQlim (exist _ f (conj e (conj n (conj n0 n1)))) (Pos.to_nat p)) as [s smaj]. unfold proj1_sig in smaj. apply (lowerUpper f (s + (1 # Pos.of_nat (S (Pos.to_nat p))))). + exact (conj e (conj n (conj n0 n1))). + apply (Qle_trans _ (s + (r-q))). * apply Qplus_le_r. apply (Qle_trans _ (1 # p)). -- unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. ++ apply le_S, Nat.le_refl. ++ discriminate. -- apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))). ++ rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l. ** reflexivity. ** apply Qinv_lt_0_compat. unfold Qminus. rewrite <- Qlt_minus_iff. exact q1. ++ unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc. rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc. ** setoid_replace ((1 # p) * (Z.pos p # 1))%Q with 1%Q. 2: reflexivity. rewrite Qmult_1_l, Qmult_1_r. apply Qlt_le_weak, pmaj. ** intro abs. apply Qlt_minus_iff in q1. rewrite abs in q1. apply (Qlt_not_le _ _ q1), Qle_refl. * apply (Qplus_le_l _ _ (q-r)). ring_simplify. exact q0. + apply smaj. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra