proposition: Lemma sum_q_pow_i : forall (q : C) (m k : nat), q <> C1 -> sum_f_C0 (fun n : nat => q_pow_i q (m + n)) k = q^m * (C1 - q ^ S k) / (C1 - q).
proof: Proof. intros q m k q_neq_1. induction k. simpl ; unfold q_pow_i. unfold Cdiv ; rewrite Cmult_assoc. rewrite Cmult_1_r, Cinv_r, Cmult_1_r. rewrite Nat.add_0_r ; reflexivity. intro Hf ; apply q_neq_1 ; intuition (auto with complex). simpl sum_f_C0 ; rewrite IHk ; clear IHk. unfold Cdiv, q_pow_i ; simpl. replace (q ^ (m + S k)) with (q ^ m * (q ^ (S k))). repeat rewrite Cmult_assoc ; rewrite <- Cmult_add_distr_l ; apply Cmult_eq_compat_l. replace (q ^ S k) with ((q ^ S k * (C1 - q)) * / (C1 - q)). simpl ; auto with complex. field ; intro Hf ; apply q_neq_1 ; intuition (auto with complex). rewrite Cmult_assoc, Cinv_r, Cmult_1_r. reflexivity. intro Hf ; apply q_neq_1 ; intuition (auto with complex). induction k. replace (m + 1)%nat with (S m) by ring ; simpl. rewrite Cmult_1_r. field. replace (m + S (S k))%nat with (S (m + S k)) by ring ; simpl ; rewrite <- IHk ; simpl ; field. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia