proposition: Lemma Rpower_nonzero : forall (x : R) (n : nat), 0 < x -> Rpower x (INR n) <> 0.
proof: Proof. intros x n H. rewrite (Rpower_pow n x H). exact (pow_nonzero x n (not_eq_sym (Rlt_not_eq 0 x H))). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra