proposition: Theorem mag_mult_bpow : forall x e, x <> 0%R -> (mag (x * bpow e) = mag x + e :>Z)%Z.
proof: Proof. intros x e Zx. destruct (mag x) as (ex, Ex) ; simpl. specialize (Ex Zx). apply mag_unique. rewrite Rabs_mult. rewrite (Rabs_pos_eq (bpow e)) by apply bpow_ge_0. split. replace (ex + e - 1)%Z with (ex - 1 + e)%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. apply Ex. rewrite bpow_plus. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Ex. Qed.
imports: Coq(Psatz Reals ZArith) Zaux