proposition: Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
proof: Proof. intro; induction n as [| n Hrecn]. - reflexivity. - replace (2 * S n)%nat with (2 + 2 * n)%nat by ring. rewrite pow_add; rewrite Hrecn; simpl; ring. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac