proposition: Lemma mag_minus_separated : forall fexp : Z -> Z, Valid_exp fexp -> forall x y, 0 < x -> 0 < y -> y < x -> bpow (mag x - 1) < x -> generic_format beta fexp x -> (mag y <= fexp (mag x))%Z -> (mag (x - y) = mag x :> Z).
proof: Proof. intros fexp Vfexp x y Px Py Yltx Xgtpow Fx Ly. apply mag_unique. split. - apply Rabs_ge; right. assert (Hy : y < ulp beta fexp (bpow (mag x - 1))). { rewrite ulp_bpow. replace (_ + _)%Z with (mag x : Z) by ring. rewrite <- (Rabs_right y); [|now apply Rle_ge; apply Rlt_le]. apply Rlt_le_trans with (bpow (mag y)). - apply bpow_mag_gt. - now apply bpow_le. } apply (Rplus_le_reg_r y); ring_simplify. apply Rle_trans with (bpow (mag x - 1) + ulp beta fexp (bpow (mag x - 1))). + now apply Rplus_le_compat_l; apply Rlt_le. + rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0]. apply succ_le_lt; [apply Vfexp|idtac|exact Fx|assumption]. apply (generic_format_bpow beta fexp (mag x - 1)). replace (_ + _)%Z with (mag x : Z) by ring. cut (fexp (mag x) < mag x)%Z. lia. now apply mag_generic_gt; [|now apply Rgt_not_eq|]. - rewrite Rabs_right. + apply Rlt_trans with x. * rewrite <- (Rplus_0_r x) at 2. apply Rplus_lt_compat_l. rewrite <- Ropp_0. now apply Ropp_lt_contravar. * apply Rabs_lt_inv. apply bpow_mag_gt. + lra. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ