proposition: Lemma Cpow_Cre_4_2 : forall n r, Cre ((0%R +i r) ^ (4 * n + 2)) = (- r ^ (4 * n + 2))%R.
proof: Proof. intros. rewrite Cpow_add. rewrite Cre_mul. rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. ring_simplify. simpl ( Cre ((0%R +i r) ^ 2)). ring_simplify. rewrite Rdef_pow_add. ring. Qed.
imports: Ctacfield Cbase Cpow Lia