proposition: Lemma sum_f_C0_reindex : forall (n : nat) (f : nat -> C), (f O) + sum_f_C0 (fun k : nat => f (S k)) n = sum_f_C0 f (S n).
proof: Proof. intros n f. induction n. simpl. ring. simpl. rewrite <- Cadd_assoc. rewrite IHn. simpl. ring. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia