proposition: Lemma sum_pow : forall (q : R) (m k : nat), q <> 1 -> sum_f_R0 (fun i : nat => q ^ (m + i)) k = q^m * (1 - q ^ S k) / (1 - q).
proof: Proof. intros q m k q_neq_1. induction m. assert (H := tech3 q k q_neq_1) ; rewrite Rmult_1_l ; rewrite <- H ; unfold pow ; simpl ; apply sum_eq ; intros i i_ub ; intuition. replace (sum_f_R0 (fun i : nat => pow q (S m + i)) k) with (q * (sum_f_R0 (fun i : nat => pow q (m + i)) k)). rewrite IHm ; simpl ; unfold Rdiv ; repeat (rewrite Rmult_assoc) ; repeat (apply Rmult_eq_compat_l) ; reflexivity. clear ; induction k. simpl ; intuition. simpl ; rewrite Rmult_plus_distr_l ; rewrite IHk ; apply Rplus_eq_compat_l ; apply Rmult_eq_compat_l. unfold pow ; replace (k + S m)%nat with (S (k + m))%nat by intuition ; simpl ; reflexivity. Qed.
imports: Reals MyRIneq Fourier Lia Lra Rsequence_usual_facts