proposition: Lemma pred_FLX_exact_shift : forall beta prec, Prec_gt_0 prec -> forall x e, pred beta (FLX_exp prec) (x * bpow beta e) = pred beta (FLX_exp prec) x * bpow beta e.
proof: Proof. intros beta prec Iprec_gt_0 x e. unfold pred. rewrite <-Ropp_mult_distr_l. f_equal. rewrite Ropp_mult_distr_l. now apply succ_FLX_exact_shift. 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