proposition: Theorem bpow_plus : forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R.
proof: Proof. intros. repeat rewrite bpow_powerRZ. apply powerRZ_add. apply Rgt_not_eq. apply radix_pos. Qed.
imports: Coq(Psatz Reals ZArith) Zaux