proposition: Lemma Cpow_Cre_4_0 : forall n r, Cre ((0%R +i r) ^ (4 * n)) = (r ^ (4 * n))%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 Cre_mul in *. simpl (Cim (r ^ 4 +i 0))%R. ring_simplify. rewrite IHn. simpl. field. CusingR_f. Qed.
imports: Ctacfield Cbase Cpow Lia