proposition: Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.
proof: Proof. intros; induction n as [| n Hrecn]. - right; reflexivity. - simpl; destruct (Rcase_abs x) as [Hlt|Hle]. + apply Rle_trans with (Rabs (x * x ^ n)). * apply RRle_abs. * rewrite Rabs_mult. apply Rmult_le_compat_l. -- apply Rabs_pos. -- right; symmetry; apply RPow_abs. + pattern (Rabs x) at 1; rewrite (Rabs_right x Hle); apply Rmult_le_compat_l. * apply Rge_le; exact Hle. * apply Hrecn. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac