proposition: Lemma Cpow_Cim_4_1 : forall n r, Cim ((0%R +i r) ^ (4 * n + 1)) = (r ^ (4 * n + 1))%R.
proof: Proof. intros. rewrite Cpow_add. rewrite Cim_mul. rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. rewrite Rdef_pow_add. simpl. ring. Qed.
imports: Ctacfield Cbase Cpow Lia