proposition: Lemma pred_FLT_le_FLX : forall beta emin prec, Prec_gt_0 prec -> forall x, pred beta (FLT_exp emin prec) x <= pred beta (FLX_exp prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x. unfold pred. apply Ropp_le_contravar. now apply succ_FLX_le_FLT. 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