proposition: Lemma equi_binom_add : forall zR zI : R, forall n n0 : nat, (n0 <= n)%nat -> ((zR +i 0%R) + (0%R +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)) = (zR +i 0%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)).
proof: Proof. intros zR zI n k Hinf. apply Cminus_diag_uniq. rewrite Cmult_add_distr_r. repeat rewrite <- Cmult_assoc. assert (H : ( forall a b c d : C, a + b - c - d = a + (b - c) - d)). intros ; ring. rewrite H. replace ((0%R +i zI) * (zR +i 0%R) ^ k * (0%R +i zI) ^ (n - k) ) with ( (zR +i 0%R) ^ k * (0%R +i zI) ^ (S n - k)) by (symmetry ; rewrite Cmult_comm ; rewrite <- Cmult_assoc ; rewrite Cmult_comm ; rewrite <- Cpow_S ; rewrite <- Nat.sub_succ_l ; intuition ;apply Hinf). replace ((zR +i 0%R) ^ k * (0%R +i zI) ^ (S n - k) * INC (fact n) * / INC (fact k * fact (n - k)) - (zR +i 0%R) ^ k * (0%R +i zI) ^ (S n - k) * INC (fact (S n)) * / INC (fact k * fact (S n - k))) with ((zR +i 0%R) ^ k * (0%R +i zI) ^ (S n - k) * (INC (fact n) * / INC (fact k * fact (n - k)) - INC (fact (S n)) * / INC (fact k * fact (S n - k)))) by ring. replace (INC (fact n) * / INC (fact k * fact (n - k)) - INC (fact (S n)) * / INC (fact k * fact (S n - k))) with (-(INC (k * fact n) / INC ( fact k * fact (S (n-k))))). 2: { rewrite <- binom_add_INC. rewrite <- Nat.sub_succ_l. unfold Cdiv. rewrite Copp_add_distr. rewrite Copp_mult_distr_l_reverse. rewrite Copp_invol. replace (fact k * fact (n-k))%nat with (fact (n-k) * fact k)%nat by ring. reflexivity. apply Hinf. apply Hinf. } assert (H1 : (forall a b c d : C, a + b - (c - d) = (a -c) + (b + d))). intros. ring. rewrite H1. rewrite Cpow_S. ring_simplify. replace ((n- k +1)%nat) with (S(n-k))%nat by ring. field_simplify. unfold Cdiv. repeat rewrite Cmult_0_l. reflexivity. apply not_0_INC. intro Habs. apply Nat.eq_mul_0 in Habs. elim Habs. apply fact_neq_0. apply fact_neq_0. Qed.
imports: Ctacfield Cbase Cprop_base Cfunctions Cpow Lia