proposition: Lemma Rpow_2_0 : forall x n, ((-x) ^ (2 * n) = x ^ (2 * n))%R.
proof: Proof. intros. induction n. intuition. replace (2 * S n)%nat with (2 + 2 * n)%nat by ring. rewrite Rdef_pow_add. replace ((-x) ^ 2)%R with (x ^ 2)%R by ring. rewrite IHn. intuition (auto with real). Qed.
imports: Ctacfield Cbase Cpow Lia