proposition: Theorem bpow_lt : forall e1 e2 : Z, (e1 < e2)%Z -> (bpow e1 < bpow e2)%R.
proof: Proof. intros e1 e2 H. replace e2 with (e1 + (e2 - e1))%Z by ring. rewrite <- (Rmult_1_r (bpow e1)). rewrite bpow_plus. apply Rmult_lt_compat_l. apply bpow_gt_0. assert (0 < e2 - e1)%Z by lia. destruct (e2 - e1)%Z ; try discriminate H0. clear. rewrite <- IZR_Zpower by easy. apply IZR_lt. now apply Zpower_gt_1. Qed.
imports: Coq(Psatz Reals ZArith) Zaux