proposition: Theorem lt_bpow : forall e1 e2 : Z, (bpow e1 < bpow e2)%R -> (e1 < e2)%Z.
proof: Proof. intros e1 e2 H. apply Z.gt_lt. apply Znot_le_gt. intros H'. apply Rlt_not_le with (1 := H). destruct (Zle_lt_or_eq _ _ H'). apply Rlt_le. now apply bpow_lt. rewrite H0. apply Rle_refl. Qed.
imports: Coq(Psatz Reals ZArith) Zaux