proposition: Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.
proof: Proof. intros x n; elim n; simpl; auto with real. intros n0 H' H'0; replace 0 with (x * 0); auto with real. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac