proposition: Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).
proof: Proof. intro; simple induction n; simpl. - symmetry; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1. - intros; rewrite H; symmetry; apply Rabs_mult. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac