proposition: Theorem MSB_monotoneAux : forall x y : float, (Fabs x <= Fabs y)%R -> Fexp x = Fexp y -> (MSB x <= MSB y)%Z.
proof: Proof. intros x y H' H'0; unfold MSB in |- *. rewrite <- H'0. cut (Fdigit radix x <= Fdigit radix y)%Z; [ unfold Z.pred in |- *; auto with zarith | idtac ]. unfold Fdigit in |- *; apply inj_le. apply digit_monotone; auto. apply le_IZR. apply Rmult_le_reg_l with (r := powerRZ radix (Fexp x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. repeat rewrite (Rmult_comm (powerRZ radix (Fexp x))); auto. pattern (Fexp x) at 2 in |- *; rewrite H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz