proposition: Lemma pow_R1_Rle : forall (x:R) (k:nat), 1 <= x -> 1 <= x ^ k.
proof: Proof. intros. induction k as [| k Hreck]. - right; reflexivity. - simpl. apply Rle_trans with (x * 1). + rewrite Rmult_1_r; assumption. + apply Rmult_le_compat_l. * left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ]. * exact Hreck. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac