proposition: Theorem LSB_le_abs : forall x : float, ~ is_Fzero x -> (Float 1 (LSB x) <= Fabs x)%R.
proof: Proof. intros x H'; apply Rle_trans with (FtoRradix (Float 1 (MSB x))). apply (oneExp_le radix); auto. apply LSB_le_MSB; auto. apply MSB_le_abs; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz