proposition: Theorem bpow_unique : forall x e1 e2, (bpow (e1 - 1) <= x < bpow e1)%R -> (bpow (e2 - 1) <= x < bpow e2)%R -> e1 = e2.
proof: Proof. intros x e1 e2 (H1a,H1b) (H2a,H2b). apply Zle_antisym ; apply bpow_lt_bpow ; apply Rle_lt_trans with x ; assumption. Qed.
imports: Coq(Psatz Reals ZArith) Zaux