proposition: Theorem bpow_le : forall e1 e2 : Z, (e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R.
proof: Proof. intros e1 e2 H. apply Rnot_lt_le. intros H'. apply Zle_not_gt with (1 := H). apply Z.lt_gt. now apply lt_bpow. Qed.
imports: Coq(Psatz Reals ZArith) Zaux