proposition: Lemma le_lower_pred_finite s m e B : le_lower (@FtoX radix2 match B2SF (Bpred (B754_finite s m e B)) with | S754_zero _ => Fzero | S754_finite s m e => Basic.Float s m e | _ => Basic.Fnan end) (@FtoX radix2 (Basic.Float s m e)).
proof: Proof. set (bx := B754_finite _ _ _ _). generalize (Bpred_correct _ _ Hprec Hmax bx (eq_refl _)). case Rlt_bool; [ |now intros ->]. intros [HR [HF HS]]. revert HR. unfold B2R at 2, bx. rewrite <-FtoR_split. case Bpred as [sx|sx| |sx mx ex Bx]; simpl; [ |now simpl..| ]. { set (x' := FtoR _ _ _ _). intro H; apply Ropp_le_contravar. refine (Rle_trans _ _ _ _ (Ulp.pred_le_id radix2 (SpecFloat.fexp FloatOps.prec emax) _)). now rewrite <-H; right. } rewrite <-FtoR_split => ->. apply Ropp_le_contravar, Ulp.pred_le_id. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig