proposition: Lemma fun_prop_bin_add_INC : forall (n : nat) (zR zI : R), (sum_f_C0 (fun n0 : nat => (zR +i zI) * ((zR +i 0%R) ^ n0 * (0%R +i zI) ^ (n - n0) * INC (fact n) / INC (fact n0 * fact (n - n0))) - (zR +i 0%R) ^ n0 * (0%R +i zI) ^ (S n - n0) * INC (fact (S n)) / INC (fact n0 * fact (S n - n0))) n) = (sum_f_C0 (fun n0 : nat => (zR +i0%R)^ S n0 * (0%R +i zI) ^ (n-n0) * INC (fact n) /INC (fact n0 * fact (n - n0)) - (zR +i 0%R) ^ n0 * (0%R +i zI)^ (S n-n0) * INC (n0*fact n) / INC (fact n0 * fact (n-n0 + 1))) n ).
proof: Proof. intros n zR zI. apply sum_f_C0_eq_seq. intros n0 H. replace (zR +i zI) with ((zR, 0%R) + (0%R, zI)) by (rewrite <- Ceq ; simpl ; intuition). generalize equi_binom_add. intro Hn1. unfold Cdiv in *. apply Hn1. exact H. Qed.
imports: Ctacfield Cbase Cprop_base Cfunctions Cpow Lia