proposition: Lemma Cpow_Cim_4_0 : forall n r, Cim ((0%R +i r) ^ (4 * n)) = 0%R.
proof: Proof. intros ; induction n. intuition. replace (4 * S n)%nat with (4 + 4 * n)%nat by ring. rewrite Cpow_add. rewrite Cpow_mul in *. replace ((0%R +i r) ^ 4) with (r ^ 4 +i 0)%R in *. rewrite Cim_mul in *. simpl (Cim (r ^ 4 +i 0))%R. ring_simplify. rewrite IHn. simpl. ring. CusingR_f. Qed.
imports: Ctacfield Cbase Cpow Lia