proposition: Theorem FSuccPropNeg : forall x y : float, (x < 0)%R -> Fcanonic radix b x -> Fcanonic radix b y -> (x < y)%R -> (FSucc x <= y)%R.
proof: Proof. intros x y H' H'0 H'1 H'2. cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H'0) ]. cut (Fbounded b y); [ intros Fb1 | apply FcanonicBound with (1 := H'1) ]. case (Rle_or_lt 0 y); intros Rle0. apply Rle_trans with (r2 := 0%R); auto. apply R0RltRleSucc; auto. cut (Fnum x <> pPred (vNum b)); [ intros N0 | idtac ]; auto with zarith. generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision)); case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); intros H'4. generalize (Z_eq_bool_correct (Fexp x) (- dExp b)); case (Z_eq_bool (Fexp x) (- dExp b)); intros H'5. replace x with (Float (Fnum x) (Fexp x)). rewrite H'4; rewrite H'5; rewrite FSuccSimpl3; auto. case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto with real. intros H'6; contradict H'6; rewrite H'5; apply Zle_not_lt; apply Fb1. intros H'6; elim H'6; intros H'7 H'8; clear H'6; replace y with (Float (Fnum y) (Fexp y)). rewrite <- H'7; rewrite H'5. generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'9; apply H'9; clear H'9; auto with arith. rewrite <- H'4; auto with zarith. case y; auto. case x; auto. rewrite FSuccSimpl2; auto. case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto with real. intros H'6; replace y with (Float (Fnum y) (Fexp y)). case (Zlt_next _ _ H'6); intros H'7. rewrite H'7. rewrite <- Zpred_succ. unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rle_monotone_exp; auto with zarith. rewrite <- (Z.opp_involutive (Fnum y)); apply IZR_le; apply Zle_Zopp. unfold pPred in |- *; apply Zle_Zpred; rewrite <- Zabs_eq_opp; auto with zarith; try apply Fb1. apply Zlt_le_weak; apply R0LtFnum with (radix := radix); auto with zarith. apply Rlt_le; auto with real. unfold FtoRradix in |- *; apply FcanonicNegFexpRlt with (3 := pGivesBound); auto. apply Rlt_le; auto. rewrite <- FSuccSimpl2; auto. apply R0RltRleSucc; auto. rewrite <- FSuccSimpl2; auto. apply FSuccCanonic; auto. simpl in |- *; auto. apply Zsucc_lt_reg; auto. rewrite <- Zsucc_pred; auto with zarith. case y; auto. intros H'6; elim H'6; intros H'7 H'8; clear H'6; apply Rlt_le. contradict H'8; rewrite H'4. apply Zle_not_lt. replace (Fnum y) with (- Z.abs (Fnum y))%Z. apply Zle_Zopp. apply pNormal_absolu_min with (3 := pGivesBound); auto. case H'1; auto. intros H'6; contradict H'5; rewrite H'7; apply H'6. rewrite Zabs_eq_opp. ring. apply R0LeFnum with (radix := radix); auto with zarith. apply Rlt_le; auto. rewrite FSuccSimpl4; auto. case FcanonicLtNeg with (p := x) (q := y) (3 := pGivesBound); auto. apply Rlt_le; auto with real. intros H'5; apply Rlt_le; auto. unfold FtoRradix in |- *; apply FcanonicNegFexpRlt with (3 := pGivesBound); auto. apply Rlt_le; auto. rewrite <- FSuccSimpl4; auto. apply R0RltRleSucc; auto. rewrite <- FSuccSimpl4; auto. apply FSuccCanonic; auto. intros H'5; elim H'5; intros H'6 H'7; clear H'5. replace y with (Float (Fnum y) (Fexp y)). rewrite H'6. generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'8; apply H'8; clear H'8; auto with zarith arith. case y; auto. apply Z.lt_neq. apply Z.lt_trans with 0%Z; auto with zarith. apply R0LtFnum with (radix := radix); auto with zarith. unfold pPred in |- *; apply Zlt_succ_pred. replace (Z.succ 0) with (Z_of_nat 1); [ apply (vNumbMoreThanOne radix) with (precision := precision) | simpl in |- * ]; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz