proposition: Lemma DRealReprQup : forall (x : DReal) (q : Q), proj1_sig x q = false -> CRealLe (DRealRepr x) (inject_Q q).
proof: Proof. intros x q H [p pmaj]. unfold inject_Q, DRealRepr, CReal_of_DReal_seq in pmaj. do 2 rewrite CReal_red_seq in pmaj. destruct (DRealQlimExp2 x (Z.to_nat (- p))) as [r rmaj]. destruct x as [f low]. unfold proj1_sig in pmaj, rmaj, H. apply proj1 in rmaj. pose proof UpperAboveLower f _ _ low rmaj H as Hrltse. 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