proposition: Lemma mag_minus_lb : forall x y, (0 < x)%R -> (0 < y)%R -> (mag y <= mag x - 2)%Z -> (mag x - 1 <= mag (x - y))%Z.
proof: Proof. assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|lia]|]. destruct (mag x) as (ex,Hex). destruct (mag y) as (ey,Hey). simpl in Hln |- *. destruct Hex as (Hex,_); [now apply Rgt_not_eq|]. destruct Hey as (_,Hey); [now apply Rgt_not_eq|]. assert (Hbx : (bpow (ex - 2) + bpow (ex - 2) <= x)%R). { ring_simplify. apply Rle_trans with (bpow (ex - 1)). - replace (ex - 1)%Z with (ex - 2 + 1)%Z by ring. rewrite bpow_plus_1. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. now apply IZR_le. - now rewrite Rabs_right in Hex; [|apply Rle_ge; apply Rlt_le]. } assert (Hby : (y < bpow (ex - 2))%R). { apply Rlt_le_trans with (bpow ey). now rewrite Rabs_right in Hey; [|apply Rle_ge; apply Rlt_le]. now apply bpow_le. } assert (Hbxy : (bpow (ex - 2) <= x - y)%R). { apply Ropp_lt_contravar in Hby. apply Rlt_le in Hby. replace (bpow (ex - 2))%R with (bpow (ex - 2) + bpow (ex - 2) - bpow (ex - 2))%R by ring. now apply Rplus_le_compat. } apply mag_ge_bpow. replace (ex - 1 - 1)%Z with (ex - 2)%Z by ring. now apply Rabs_ge; right. Qed.
imports: Coq(Psatz Reals ZArith) Zaux