proposition: Lemma pred_round_FLT_le_FLX : forall beta emin prec, Prec_gt_0 prec -> forall rnd, Valid_rnd rnd -> forall x, generic_format beta (FLX_exp prec) x -> pred beta (FLT_exp emin prec) (Generic_fmt.round beta (FLT_exp emin prec) rnd x) <= pred beta (FLX_exp prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 rnd Ivalid_rnd x Hx. unfold pred. apply Ropp_le_contravar. set (rnd' := fun x => Z.opp (rnd (- x))). replace (- Generic_fmt.round _ _ _ _) with (Generic_fmt.round beta (FLT_exp emin prec) rnd' (- x)). 2: { unfold Generic_fmt.round, scaled_mantissa, F2R. simpl. unfold rnd'. now rewrite cexp_opp, <-Ropp_mult_distr_l, Ropp_involutive, Ropp_mult_distr_l, <-opp_IZR. } apply succ_round_FLX_le_FLT; [easy | | now apply generic_format_opp]. apply Build_Valid_rnd; unfold rnd'. - intros x' y' Hx'y'. rewrite <-Z.opp_le_mono. apply Ivalid_rnd. lra. - intros n. rewrite <-opp_IZR. apply Z.opp_inj. rewrite Z.opp_involutive. apply Ivalid_rnd. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper