proposition: Theorem LSB_le_MSB : forall x : float, ~ is_Fzero x -> (LSB x <= MSB x)%Z.
proof: Proof. intros x H'; unfold LSB, MSB in |- *. apply Zle_Zpred. cut (maxDiv (Fnum x) (Fdigit radix x) < Fdigit radix x); auto with zarith. apply maxDivLt; auto. unfold Fdigit in |- *; apply NotDividesDigit; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz