proposition: Theorem MSB_le_abs : forall x : float, ~ is_Fzero x -> (Float 1 (MSB x) <= Fabs x)%R.
proof: Proof. intros x H'; unfold MSB, FtoRradix, FtoR in |- *; simpl in |- *. replace (Z.pred (Fdigit radix x + Fexp x)) with (Z.pred (Fdigit radix x) + Fexp x)%Z; [ idtac | unfold Z.pred in |- *; ring ]. rewrite powerRZ_add; auto with real zarith arith. rewrite Rmult_1_l. repeat rewrite (fun r : R => Rmult_comm r (powerRZ radix (Fexp x))). apply Rmult_le_compat_l; auto with real zarith. now apply powerRZ_le, IZR_lt. rewrite <- inj_pred; auto with real zarith. rewrite <- Zpower_nat_Z_powerRZ; auto. apply IZR_le; auto. unfold Fdigit in |- *; auto with arith. apply digitLess; auto. unfold Fdigit in |- *. rewrite Nat.neq_0_lt_0; apply digitNotZero; auto. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz