proposition: Lemma CRealLowerBoundSpec: forall (x : CReal) (xPos : 0<x), forall p : Z, (p <= (CRealLowerBound x xPos))%Z -> (seq x p > 2^(CRealLowerBound x xPos))%Q.
proof: Proof. intros x xPos p Hp. unfold CRealLowerBound in *. destruct xPos as [n Hn]; unfold proj1_sig in *. unfold inject_Q in Hn; rewrite CReal_red_seq in Hn. ring_simplify in Hn. pose proof cauchy x n n p ltac:(lia) ltac:(lia) as Hxbnd. rewrite Qabs_Qlt_condition in Hxbnd. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra