proposition: Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
proof: Proof. intros x n; elim n; simpl; auto with real. - intros H' H'0; exfalso. apply (Nat.lt_irrefl 0); assumption. - intros n0; case n0. + simpl; rewrite Rmult_1_r; auto. + intros n1 H' H'0 H'1. replace 1 with (1 * 1); auto with real. apply Rlt_trans with (r2 := x * 1); auto with real. apply Rmult_lt_compat_l; auto with real. * apply Rlt_trans with (r2 := 1); auto with real. * apply H'; auto with arith. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac