proposition: Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.
proof: Proof. intro; induction n as [| n Hrecn]. - simpl; apply Rabs_R1. - replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ]. rewrite Rabs_mult. rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r. change (-1) with (-(1)). rewrite Rabs_Ropp; apply Rabs_R1. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac