proposition: Theorem FUlp_Le_LSigB : forall x : float, Fbounded b x -> (Fulp x <= Float 1 (LSB radix x))%R.
proof: Proof. intros x H; unfold is_Fzero, Fulp, Fnormalize in |- *; case (Z_zerop (Fnum x)); intros ZH. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite Rmult_1_l. apply Rle_powerRZ. apply IZR_le; lia. apply Z.le_trans with (Fexp x); auto. case H; auto. apply Fexp_le_LSB; auto. rewrite LSB_shift with (n := min (precision - Fdigit radix x) (Z.abs_nat (dExp b + Fexp x))); auto. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite Rmult_1_l. apply Rle_powerRZ; auto with arith. apply IZR_le; lia. exact (Fexp_le_LSB radix (Fshift radix (min (precision - Fdigit radix x) (Z.abs_nat (dExp b + Fexp x))) x)). Qed.
imports: Reals ZArith List PeanoNat Psatz