proposition: Theorem bpow_lt_bpow : forall e1 e2, (bpow (e1 - 1) < bpow e2)%R -> (e1 <= e2)%Z.
proof: Proof. intros e1 e2 He. rewrite (Zsucc_pred e1). apply Zlt_le_succ. now apply lt_bpow. Qed.
imports: Coq(Psatz Reals ZArith) Zaux