proposition: Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)), CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos)) == inject_Q (1 # b).
proof: Proof. intros. apply (CReal_mult_eq_reg_l (inject_Q (Z.pos b # 1))). - right. apply CReal_injectQPos. exact pos. - rewrite CReal_mult_comm, CReal_inv_l. apply CRealEq_diff. intro n. simpl. do 2 rewrite Pos.mul_1_r. rewrite Z.pos_sub_diag. pose proof Qpower_pos 2 n ltac:(lra). rewrite Z.abs_0, Qreduce_zero. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra