proposition: Lemma sum_f_C0_eq_seq : forall (n : nat) (f g : nat -> C), (forall m : nat, (m <= n)%nat -> f m = g m) -> sum_f_C0 f n = sum_f_C0 g n.
proof: Proof. intros n f g H. induction n. simpl. apply H. intuition. simpl. rewrite IHn. rewrite H with (S n) ; intuition. intros m H2. apply H. intuition. Qed.
imports: Cbase Cnorm Ctacfield Cprop_base Cpow Lia