proposition: Lemma Cpow_Cre_4_1 : forall n r, Cre ((0%R +i r) ^ (4 * n + 1)) = 0%R.
proof: Proof. intros. rewrite Cpow_add. rewrite Cre_mul. rewrite Cpow_Cre_4_0. rewrite Cpow_Cim_4_0. simpl ; field. Qed.
imports: Ctacfield Cbase Cpow Lia