proposition: Lemma CReal_inv_l_pos : forall (r:CReal) (Hrpos : 0 < r), (CReal_inv_pos r Hrpos) * r == 1.
proof: Proof. intros r Hrpos; apply CRealEq_diff; intros n. unfold CReal_mult, CReal_mult_seq, CReal_mult_scale; unfold CReal_inv_pos, CReal_inv_pos_seq, CReal_inv_pos_scale, CReal_inv_pos_cm; unfold inject_Q. do 3 rewrite CReal_red_seq. do 1 rewrite CReal_red_scale. simplify_seq_idx. remember (Z.min (CRealLowerBound r Hrpos) (n - scale r - 1 + 2 * CRealLowerBound r Hrpos))%Z as k. assert (0 < seq r k)%Q as Hrseqpos. { pose proof Qpower_0_lt 2 (CRealLowerBound r Hrpos)%Z ltac:(lra) as Hpow. pose proof CRealLowerBoundSpec r Hrpos k ltac:(lia) as Hlowbnd. lra. } field_simplify_Qabs; [|lra]; unfold Qdiv. rewrite Qabs_Qmult, Qabs_Qinv. apply Qle_shift_div_r. 1: apply Qabs_gt; lra. pose proof cauchy r (n + CRealLowerBound r Hrpos)%Z (n + CRealLowerBound r Hrpos - 1)%Z k as Hrbnd. pose proof CRealLowerBound_lt_scale r Hrpos as Hscale_lowbnd. specialize (Hrbnd ltac:(lia) ltac:(lia)). simplify_Qabs_in Hrbnd; simplify_Qabs. rewrite Qplus_comm in Hrbnd. apply Qlt_le_weak in Hrbnd. apply (Qle_trans _ _ _ Hrbnd). pose proof CRealLowerBoundSpec r Hrpos k ltac:(lia) as Hlowbnd. rewrite Qpower_plus; [|lra]. apply Qmult_le_compat_nonneg. { pose proof Qpower_pos 2 n; split; lra. } split. - apply Qpower_pos; lra. - rewrite Qabs_pos; [lra|]. pose proof Qpower_0_lt 2 (CRealLowerBound r Hrpos)%Z ltac:(lra) as Hpow. lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra