proposition: Lemma GeoCvZero : forall {R : ConstructiveReals}, CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0.
proof: Proof. intro R. assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). { induction n. - unfold INR; simpl. apply CRzero_lt_one. - unfold INR. fold (1+n)%nat. rewrite Nat2Z.inj_add. rewrite (CR_of_Q_morph R _ ((Z.of_nat 1 # 1) + (Z.of_nat n #1))). 2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus. replace (CRpow (CR_of_Q R 2) (1 + n)) with (CR_of_Q R 2 * CRpow (CR_of_Q R 2) n). 2: reflexivity. rewrite CR_double. apply CRplus_le_lt_compat. 2: exact IHn. simpl. apply CRpow_ge_one. apply CR_of_Q_le. discriminate. } intros p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. rewrite CRabs_right. 2: apply CRpow_ge_zero; apply CR_of_Q_le; discriminate. apply CRlt_asym. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))). - apply CR_of_Q_lt. reflexivity. - rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1). 2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity. apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)). + apply CRpow_gt_zero. apply CR_of_Q_lt. reflexivity. + rewrite CRmult_assoc. rewrite CRpow_mult. rewrite (CRpow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), CRpow_one. * rewrite CRmult_1_r, CRmult_1_l. apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H. apply CR_of_Q_le. unfold Qle,Qnum,Qden. do 2 rewrite Z.mul_1_r. rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0. * rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. -- reflexivity. -- reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum