proposition: Lemma tech3 : forall (k:R) (N:nat), k <> 1 -> sum_f_R0 (fun i:nat => k ^ i) N = (1 - k ^ S N) / (1 - k).
proof: Proof. intros; cut (1 - k <> 0). - intro; induction N as [| N HrecN]. + simpl; rewrite Rmult_1_r; unfold Rdiv; rewrite Rinv_r. * reflexivity. * apply H0. + replace (sum_f_R0 (fun i:nat => k ^ i) (S N)) with (sum_f_R0 (fun i:nat => k ^ i) N + k ^ S N); [ idtac | reflexivity ]; rewrite HrecN; replace ((1 - k ^ S N) / (1 - k) + k ^ S N) with ((1 - k ^ S N + (1 - k) * k ^ S N) / (1 - k)). * apply Rmult_eq_reg_l with (1 - k). -- unfold Rdiv; do 2 rewrite <- (Rmult_comm (/ (1 - k))); repeat rewrite <- Rmult_assoc; rewrite Rinv_r; [ do 2 rewrite Rmult_1_l; simpl; ring | apply H0 ]. -- apply H0. * unfold Rdiv; rewrite Rmult_plus_distr_r; rewrite (Rmult_comm (1 - k)); repeat rewrite Rmult_assoc; rewrite Rinv_r. -- rewrite Rmult_1_r; reflexivity. -- apply H0. - apply Rminus_eq_contra; red; intro; elim H; symmetry ; assumption. Qed.
imports: Rbase Rfunctions Rseries Rcomplete