proposition: Lemma format_xminusk: format xk.
proof: Proof. Proof with auto with typeclass_instances. apply generic_format_FLX. unfold generic_format in Fx. exists (Float beta (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) - k) (cexp beta (FLX_exp prec) x)). unfold xk; rewrite Fx at 1; unfold F2R; simpl. rewrite minus_IZR; ring_simplify. apply f_equal. rewrite ulp_neq_0; try now apply Rgt_not_eq. apply Rmult_comm; apply f_equal. simpl. rewrite Z.abs_eq. apply Z.le_lt_trans with (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) - 0)%Z. apply Zplus_le_compat_l. lia. rewrite Zminus_0_r. apply lt_IZR. apply Rmult_lt_reg_r with (bpow (cexp beta (FLX_exp prec) x)). apply bpow_gt_0. apply Rle_lt_trans with x. rewrite Fx at 3. right; unfold F2R; reflexivity. rewrite IZR_Zpower. rewrite <- bpow_plus. unfold cexp, FLX_exp. replace (prec + (mag beta x - prec))%Z with (mag beta x+0)%Z by ring. rewrite Zplus_0_r. apply Rle_lt_trans with (Rabs x). apply RRle_abs. apply bpow_mag_gt... lia. apply le_IZR. apply Rmult_le_reg_r with (bpow (cexp beta (FLX_exp prec) x)). apply bpow_gt_0. rewrite Rmult_0_l. apply Rle_trans with xk. left; apply xkpos. right; unfold xk; rewrite Fx at 1; unfold F2R; simpl; rewrite minus_IZR; ring_simplify. apply f_equal. rewrite ulp_neq_0; try now apply Rgt_not_eq. apply Rmult_comm; apply f_equal. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic)