proposition: Theorem abs_lt_MSB : forall x : float, (Fabs x < Float 1 (Z.succ (MSB x)))%R.
proof: Proof. intros x. rewrite (MSB_abs x). unfold MSB, FtoRradix, FtoR in |- *. rewrite <- Zsucc_pred; simpl in |- *. rewrite powerRZ_add; auto with real zarith. rewrite Rmult_1_l. repeat rewrite (fun r : R => Rmult_comm r (powerRZ radix (Fexp x))). apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; easy. rewrite <- Zpower_nat_Z_powerRZ; auto with arith. apply IZR_lt. unfold Fdigit in |- *; auto with arith. unfold Fabs in |- *; simpl in |- *. pattern (Z.abs (Fnum x)) at 1 in |- *; rewrite <- (Z.abs_eq (Z.abs (Fnum x))); auto with zarith. apply digitMore; easy. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz