proposition: Lemma CRealLowerBound_lt_scale: forall (r : CReal) (Hrpos : 0 < r), (CRealLowerBound r Hrpos < scale r)%Z.
proof: Proof. intros r Hrpos. pose proof CRealLowerBoundSpec r Hrpos (CRealLowerBound r Hrpos) ltac:(lia) as Hlow. pose proof bound r (CRealLowerBound r Hrpos) as Hup; unfold QBound in Hup. apply Qabs_Qlt_condition in Hup. destruct Hup as [_ Hup]. pose proof Qlt_trans _ _ _ Hlow Hup as Hpow. apply Qpower_lt_compat_l_inv in Hpow. 2: lra. exact Hpow. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra