proposition: Lemma Cpow_add_dev : forall z : C, forall n : nat, ((z ^ n)%C = (sum_f_C0 (fun k => (Cre z +i 0%R)^k * (0%R +i Cim z) ^ (n-k) * INC (fact n)/INC ((fact k) * fact (n-k))) n))%C.
proof: Proof. intros z. induction n. simpl. CusingR_f. destruct z as (zR, zI). replace ((zR, zI) ^ S n) with ((zR, zI) * (zR, zI) ^ n) by (simpl; reflexivity). rewrite IHn. replace (Cre (zR, zI)) with zR by (simpl; reflexivity). replace (Cim (zR, zI)) with zI by (simpl; reflexivity). rewrite sum_f_C0_mult. rewrite sum_f_C0_simpl. apply Cminus_diag_uniq. assert (H4 : ( forall a b c : C, a - (b + c) = (a - b) - c)). intros; ring. rewrite H4. rewrite <- sum_f_C0_minus_compat. replace (zR, zI) with (zR +i zI) by reflexivity. replace (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) with (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 ) by (rewrite fun_prop_bin_add_INC ; reflexivity). rewrite sum_f_C0_minus_compat. destruct n. CusingR_f. rewrite sum_f_C0_simpl. rewrite <- sum_f_C0_reindex. replace (sum_f_C0 (fun n0 : nat => (zR +i 0%R) ^ S n0 * (0%R +i zI) ^ (S n - n0) * INC (fact (S n)) / INC (fact n0 * fact (S n - n0))) n) with (sum_f_C0 (fun k : nat => (zR +i 0%R) ^ S k * (0%R +i zI) ^ (S (S n) - S k) * INC (S k * fact (S n)) / INC (fact (S k) * fact (S n - S k + 1))) n). 2: { apply sum_f_C0_eq_seq. intros m H. repeat rewrite fact_simpl. repeat rewrite mult_INC. replace (S n - S m + 1)%nat with (S n - m)%nat by intuition lia. replace (S (S n) - S m)%nat with (S n - m)%nat by intuition. field. split ; try split ; apply not_0_INC ; try apply fact_neq_0 ; intuition lia. } ring_simplify. replace (S n - S n)%nat with O by intuition. replace (S (S n) - S (S n))%nat with O by intuition. repeat rewrite fact_simpl. repeat rewrite mult_INC. simpl (INC 0). field_simplify. unfold Cdiv. repeat rewrite Cmult_0_r. rewrite Cmult_0_l. reflexivity. split ; try split ; try split ; try split ; try apply not_0_INC ; try apply fact_neq_0 ; intuition lia. Qed.
imports: Ctacfield Cbase Cprop_base Cfunctions Cpow Lia