proposition: Theorem mag_bpow : forall e, (mag (bpow e) = e + 1 :> Z)%Z.
proof: Proof. intros e. apply mag_unique. rewrite Rabs_right. replace (e + 1 - 1)%Z with e by ring. split. apply Rle_refl. apply bpow_lt. apply Zlt_succ. apply Rle_ge. apply bpow_ge_0. Qed.
imports: Coq(Psatz Reals ZArith) Zaux