proposition: Lemma Cpow_Cre_Cim_0 : forall r n, Cre ((r +i 0%R) ^ n) = (r ^ n)%R /\ Cim ((r +i 0%R) ^ n) = 0%R.
proof: Proof. induction n. compute ; split ; reflexivity. replace ((r +i 0%R) ^ S n) with ((r +i 0%R) ^ n * (r +i 0%R)) by (rewrite Cpow_S ; intuition). simpl. destruct IHn as (IHn1, IHn2). split ; simpl ; rewrite IHn1 ; rewrite IHn2 ; field. Qed.
imports: Ctacfield Cbase Cpow Lia