proposition: Lemma CReal_inv_pos_bound : forall (x : CReal) (Hxpos : 0 < x), QBound (CReal_inv_pos_seq x Hxpos) (CReal_inv_pos_scale x Hxpos).
proof: Proof. intros x Hxpos n. unfold CReal_inv_pos_seq, CReal_inv_pos_scale, CReal_inv_pos_cm. remember (CRealLowerBound x Hxpos) as k. pose proof CRealLowerBoundSpec x Hxpos (Z.min k (n + 2 * k))%Z ltac:(lia) as Hlb. rewrite <- Heqk in Hlb. rewrite Qabs_pos. 2: apply Qinv_le_0_compat; pose proof Qpower_pos 2 k; lra. rewrite Qpower_opp; apply -> Qinv_lt_contravar. - exact Hlb. - pose proof Qpower_0_lt 2 k; lra. - apply Qpower_0_lt; lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra