proposition: Lemma mag_mult : forall x y, (x <> 0)%R -> (y <> 0)%R -> (mag x + mag y - 1 <= mag (x * y) <= mag x + mag y)%Z.
proof: Proof. intros x y Hx Hy. destruct (mag x) as (ex, Hx2). destruct (mag y) as (ey, Hy2). simpl. destruct (Hx2 Hx) as (Hx21,Hx22); clear Hx2. destruct (Hy2 Hy) as (Hy21,Hy22); clear Hy2. assert (Hxy : (bpow (ex + ey - 1 - 1) <= Rabs (x * y))%R). { replace (ex + ey -1 -1)%Z with (ex - 1 + (ey - 1))%Z; [|ring]. rewrite bpow_plus. rewrite Rabs_mult. now apply Rmult_le_compat; try apply bpow_ge_0. } assert (Hxy2 : (Rabs (x * y) < bpow (ex + ey))%R). { rewrite Rabs_mult. rewrite bpow_plus. apply Rmult_le_0_lt_compat; try assumption. now apply Rle_trans with (bpow (ex - 1)); try apply bpow_ge_0. now apply Rle_trans with (bpow (ey - 1)); try apply bpow_ge_0. } split. - now apply mag_ge_bpow. - apply mag_le_bpow. + now apply Rmult_integral_contrapositive_currified. + assumption. Qed.
imports: Coq(Psatz Reals ZArith) Zaux