proposition: Theorem bpow_exp : forall e : Z, bpow e = exp (IZR e * ln (IZR r)).
proof: Proof. assert (forall e, bpow (Zpos e) = exp (IZR (Zpos e) * ln (IZR r))). intros e. unfold bpow. rewrite Zpower_pos_nat. rewrite <- positive_nat_Z. rewrite <- INR_IZR_INZ. induction (nat_of_P e). rewrite Rmult_0_l. now rewrite exp_0. rewrite Zpower_nat_S. rewrite S_INR. rewrite Rmult_plus_distr_r. rewrite exp_plus. rewrite Rmult_1_l. rewrite exp_ln. rewrite <- IHn. rewrite <- mult_IZR. now rewrite Zmult_comm. apply radix_pos. intros [|e|e]. rewrite Rmult_0_l. now rewrite exp_0. apply H. unfold bpow. change (IZR (Zpower_pos r e)) with (bpow (Zpos e)). rewrite H. rewrite <- exp_Ropp. rewrite <- Ropp_mult_distr_l_reverse. now rewrite <- opp_IZR. Qed.
imports: Coq(Psatz Reals ZArith) Zaux