proposition: Lemma DRealReprQ : forall (x : DReal) (q : Q), proj1_sig x q = true -> CRealLt (inject_Q q) (DRealRepr x).
proof: Proof. intros x q H. destruct (DRealOpen x q H) as [r rmaj]. destruct (QarchimedeanLowExp2_Z ((1#4)*(r - q))) as [p pmaj]. 1: lra. exists (p)%Z. destruct x as [f low]; unfold DRealRepr, CReal_of_DReal_seq, inject_Q; do 2 rewrite CReal_red_seq. destruct (DRealQlimExp2 (exist _ f low) (Z.to_nat (-p))) as [s smaj]. unfold proj1_sig in smaj, rmaj, H |- * . rewrite <- (Qmult_lt_l _ _ 4%Q) in pmaj by lra. setoid_replace (4 * ((1 # 4) * (r - q)))%Q with (r-q)%Q in pmaj by ring. apply proj2 in rmaj. apply proj2 in smaj. pose proof UpperAboveLower f _ _ low rmaj smaj as Hrltse; clear rmaj smaj. pose proof Qpower_2_invneg_le_pow p as Hpowcut. pose proof Qpower_0_lt 2 p ltac:(lra) as Hpowpos. lra. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra