proposition: Lemma succ_FLT_shift_ge : 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, succ beta (FLT_exp emin prec) x * bpow beta e <= succ beta (FLT_exp emin prec) (Generic_fmt.round beta (FLT_exp emin prec) rnd (x * bpow beta e)).
proof: Proof. intros beta emin prec Iprec_gt_0 rnd Ivalid_rnd x Hformat_x Hmin_x e. rewrite <-(succ_FLX_eq_FLT_large _ _ _ _ x) by easy. rewrite <-succ_FLX_exact_shift by easy. apply succ_round_FLX_le_FLT; [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