proposition: Lemma mag_div : forall x y : R, x <> 0%R -> y <> 0%R -> (mag x - mag y <= mag (x / y) <= mag x - mag y + 1)%Z.
proof: Proof. intros x y Px Py. destruct (mag x) as (ex,Hex). destruct (mag y) as (ey,Hey). simpl. unfold Rdiv. assert (Heiy : (bpow (- ey) < Rabs (/ y) <= bpow (- ey + 1))%R). { rewrite Rabs_Rinv by easy. split. - rewrite bpow_opp. apply Rinv_lt_contravar. + apply Rmult_lt_0_compat. now apply Rabs_pos_lt. now apply bpow_gt_0. + now apply Hey. - replace (_ + _)%Z with (- (ey - 1))%Z by ring. rewrite bpow_opp. apply Rinv_le; [now apply bpow_gt_0|]. now apply Hey. } split. - apply mag_ge_bpow. replace (_ - _)%Z with (ex - 1 - ey)%Z by ring. unfold Zminus at 1; rewrite bpow_plus. rewrite Rabs_mult. apply Rmult_le_compat. + now apply bpow_ge_0. + now apply bpow_ge_0. + now apply Hex. + now apply Rlt_le; apply Heiy. - apply mag_le_bpow. + apply Rmult_integral_contrapositive_currified. exact Px. now apply Rinv_neq_0_compat. + replace (_ + 1)%Z with (ex + (- ey + 1))%Z by ring. rewrite bpow_plus. apply Rlt_le_trans with (bpow ex * Rabs (/ y))%R. * rewrite Rabs_mult. apply Rmult_lt_compat_r. apply Rabs_pos_lt. now apply Rinv_neq_0_compat. now apply Hex. * apply Rmult_le_compat_l; [now apply bpow_ge_0|]. apply Heiy. Qed.
imports: Coq(Psatz Reals ZArith) Zaux