proposition: Lemma CReal_inv_0_lt_compat : forall (r : CReal) (rnz : r # 0), 0 < r -> 0 < ((/ r) rnz).
proof: Proof. intros r Hrnz Hrpos; unfold CReal_inv; cbn. destruct Hrnz. - exfalso. apply CRealLt_asym in Hrpos. contradiction. - unfold CRealLt. exists (- (scale r) - 1)%Z. unfold inject_Q; rewrite CReal_red_seq; simplify_Qlt. unfold CReal_inv_pos; rewrite CReal_red_seq. unfold CReal_inv_pos_seq. pose proof bound r as Hrbnd; unfold QBound in Hrbnd. rewrite Qpower_minus by lra. field_simplify (2 * (2 ^ (- scale r) / 2 ^ 1))%Q. rewrite Qpower_opp; apply -> Qinv_lt_contravar. + setoid_rewrite Qabs_Qlt_condition in Hrbnd. specialize (Hrbnd (CReal_inv_pos_cm r c (- scale r - 1))%Z). lra. + apply Qpower_0_lt; lra. + unfold CReal_inv_pos_cm. pose proof CRealLowerBoundSpec r c ((Z.min (CRealLowerBound r c) (- scale r - 1 + 2 * CRealLowerBound r c)))%Z ltac:(lia) as Hlowbnd. pose proof Qpower_0_lt 2 (CRealLowerBound r c) as Hpow. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra