proposition: Lemma Rpow_2_1 : forall x n, ((-x) ^ (S (2 * n)) = - (x ^ (S (2 * n))))%R.
proof: Proof. intros. simpl. replace (n + (n + 0))%nat with (2 * n)%nat by (simpl ; reflexivity). rewrite Rpow_2_0. ring. Qed.
imports: Ctacfield Cbase Cpow Lia