proposition: Theorem le_bpow : forall e1 e2 : Z, (bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z.
proof: Proof. intros e1 e2 H. apply Znot_gt_le. intros H'. apply Rle_not_lt with (1 := H). apply bpow_lt. now apply Z.gt_lt. Qed.
imports: Coq(Psatz Reals ZArith) Zaux