proposition: Theorem pow_lt : forall (e : R) (n : nat), (0 < e)%R -> (0 < e ^ n)%R.
proof: Proof. intros e n; elim n; simpl in |- *; auto with real. intros n0 H' H'0; replace 0%R with (e * 0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz