proposition: Theorem mag_gt_bpow : forall x e, (bpow e <= Rabs x)%R -> (e < mag x)%Z.
proof: Proof. intros x e Hx. destruct (mag x) as (ex, Ex) ; simpl. apply lt_bpow. apply Rle_lt_trans with (1 := Hx). apply Ex. intros Zx. apply Rle_not_lt with (1 := Hx). rewrite Zx, Rabs_R0. apply bpow_gt_0. Qed.
imports: Coq(Psatz Reals ZArith) Zaux