proposition: Lemma pow_maj_Rabs : forall (x y:R) (n:nat), Rabs y <= x -> y ^ n <= x ^ n.
proof: Proof. intros; cut (0 <= x). - intro; apply Rle_trans with (Rabs y ^ n). + apply pow_Rabs. + induction n as [| n Hrecn]. * right; reflexivity. * simpl; apply Rle_trans with (x * Rabs y ^ n). -- do 2 rewrite <- (Rmult_comm (Rabs y ^ n)). apply Rmult_le_compat_l. ++ apply pow_le; apply Rabs_pos. ++ assumption. -- apply Rmult_le_compat_l. ++ apply H0. ++ apply Hrecn. - apply Rle_trans with (Rabs y); [ apply Rabs_pos | exact H ]. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac