proposition: Lemma FLT_ulp_le_id: forall u, bpow emin <= u -> ulp_flt u <= u.
proof: Proof. Proof with auto with typeclass_instances. intros u H. rewrite ulp_neq_0. 2: apply Rgt_not_eq, Rlt_le_trans with (2:=H), bpow_gt_0. case (Rle_or_lt (bpow (emin+prec-1)) u); intros Hu. unfold ulp; rewrite cexp_FLT_FLX. unfold cexp, FLX_exp. destruct (mag radix2 u) as (e,He); simpl. apply Rle_trans with (bpow (e-1)). apply bpow_le. unfold Prec_gt_0 in prec_gt_0_; lia. rewrite <- (Rabs_right u). apply He. apply Rgt_not_eq, Rlt_gt. apply Rlt_le_trans with (2:=Hu). apply bpow_gt_0. apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0. rewrite Rabs_right. assumption. apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0. unfold ulp; rewrite cexp_FLT_FIX. apply H. apply Rgt_not_eq, Rlt_gt. apply Rlt_le_trans with (2:=H). apply bpow_gt_0. rewrite Rabs_right. apply Rlt_le_trans with (1:=Hu). apply bpow_le; lia. apply Rle_ge, Rle_trans with (2:=H), bpow_ge_0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)