proposition: Theorem bpow_opp : forall e : Z, (bpow (-e) = /bpow e)%R.
proof: Proof. intros [|p|p]. apply eq_sym, Rinv_1. now change (-Zpos p)%Z with (Zneg p). change (-Zneg p)%Z with (Zpos p). simpl; rewrite Rinv_involutive; trivial. apply Rgt_not_eq. apply (bpow_gt_0 (Zpos p)). Qed.
imports: Coq(Psatz Reals ZArith) Zaux