proposition: Theorem MSB_monotone : forall x y : float, ~ is_Fzero x -> ~ is_Fzero y -> (Fabs x <= Fabs y)%R -> (MSB x <= MSB y)%Z.
proof: Proof. intros x y H' H'0 H'1; rewrite (MSB_abs x); rewrite (MSB_abs y). case (Zle_or_lt (Fexp (Fabs x)) (Fexp (Fabs y))); simpl in |- *; intros Zle1. rewrite MSB_shift with (x := Fabs y) (n := Z.abs_nat (Fexp (Fabs y) - Fexp (Fabs x))). apply MSB_monotoneAux; auto. unfold FtoRradix in |- *; repeat rewrite Fabs_correct; auto with real arith. rewrite FshiftCorrect; auto with real arith. repeat rewrite Fabs_correct; auto with real arith. repeat rewrite Rabs_Rabsolu; repeat rewrite <- Fabs_correct; auto with real arith. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; [ ring | auto with zarith ]. apply Fabs_Fzero; auto. rewrite MSB_shift with (x := Fabs x) (n := Z.abs_nat (Fexp (Fabs x) - Fexp (Fabs y))). apply MSB_monotoneAux; auto. unfold FtoRradix in |- *; repeat rewrite Fabs_correct; auto with real arith. rewrite FshiftCorrect; auto with real arith. repeat rewrite Fabs_correct; auto with real arith. repeat rewrite Rabs_Rabsolu; repeat rewrite <- Fabs_correct; auto with real arith. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; [ ring | auto with zarith ]. apply Fabs_Fzero; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz