proposition: Lemma pred_FLT_shift_le : forall beta emin prec, Prec_gt_0 prec -> forall rnd, Valid_rnd rnd -> forall x, generic_format beta (FLT_exp emin prec) x -> bpow beta (emin + prec - 1) < x -> forall e, pred beta (FLT_exp emin prec) (Generic_fmt.round beta (FLT_exp emin prec) rnd (x * bpow beta e)) <= pred beta (FLT_exp emin prec) x * bpow beta e.
proof: Proof. intros beta emin prec Iprec_gt_0 rnd Ivalid_rnd x Hformat_x Hinf_x e. rewrite (pred_FLT_eq_FLX_large _ _ _ _ x) by easy. rewrite <-pred_FLX_exact_shift by easy. apply pred_round_FLT_le_FLX; [easy.. |]. now apply Mult_error.mult_bpow_exact_FLX, generic_format_FLX_FLT with emin. 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