proposition: Theorem bpow_mag_gt : forall x, (Rabs x < bpow (mag x))%R.
proof: Proof. intros x. destruct (Req_dec x 0) as [Zx|Zx]. rewrite Zx, Rabs_R0. apply bpow_gt_0. destruct (mag x) as (ex, Ex) ; simpl. now apply Ex. Qed.
imports: Coq(Psatz Reals ZArith) Zaux