proposition: Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), CRsum (CRpow (CR_of_Q R (1#2))) n == CR_of_Q R 2 - CRpow (CR_of_Q R (1#2)) n.
proof: Proof. induction n. - unfold CRsum, CRpow. simpl (1%ConstructiveReals). unfold CRminus. rewrite (CR_of_Q_plus R 1 1). rewrite CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_r. reflexivity. - setoid_replace (CRsum (CRpow (CR_of_Q R (1 # 2))) (S n)) with (CRsum (CRpow (CR_of_Q R (1 # 2))) n + CRpow (CR_of_Q R (1 # 2)) (S n)). 2: reflexivity. rewrite IHn. clear IHn. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. + reflexivity. + apply (CRplus_eq_reg_l (CRpow (CR_of_Q R (1 # 2)) n + CRpow (CR_of_Q R (1 # 2)) (S n))). rewrite (CRplus_assoc _ _ (-CRpow (CR_of_Q R (1 # 2)) (S n))), CRplus_opp_r, CRplus_0_r. rewrite (CRplus_comm (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_assoc. rewrite <- (CRplus_assoc (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_opp_r, CRplus_0_l, <- CR_double. setoid_replace (CRpow (CR_of_Q R (1 # 2)) (S n)) with (CR_of_Q R (1 # 2) * CRpow (CR_of_Q R (1 # 2)) n). 2: reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. * apply CRmult_1_l. * reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits ConstructiveSum