proposition: Theorem FSuccPropPos : forall x y : float, (0 <= x)%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 FcanonicLtPos with (p := x) (q := y) (3 := pGivesBound); auto. case (Z.eq_dec (Fnum x) (pPred (vNum b))); intros H'4. rewrite FSuccSimpl1; auto. intros H'5; case (Zlt_next _ _ H'5); intros H'6. replace y with (Float (Fnum y) (Fexp y)). rewrite H'6. generalize Fle_Zle; unfold Fle, FtoRradix in |- *; intros H'7; apply H'7; clear H'7; auto with arith. rewrite <- (Z.abs_eq (Fnum y)); auto with zarith. apply pNormal_absolu_min with (b := b); auto. case H'1; auto with zarith. intros H'7; contradict H'5; apply Zle_not_lt. replace (Fexp y) with (- dExp b)%Z; try apply Fb0. case H'7; intros H'8 (H'9, H'10); auto. apply LeR0Fnum with (radix := radix); auto with zarith. apply Rle_trans with (r2 := FtoR radix x); auto with real. case y; auto. apply Rlt_le; auto. unfold FtoRradix in |- *; apply FcanonicPosFexpRlt with (3 := pGivesBound); auto. apply LeFnumZERO with (radix := radix); auto with zarith. simpl in |- *; auto with zarith. apply Zlt_le_weak; apply nNormPos; try easy. apply Rle_trans with (r2 := FtoR radix x); auto with real. rewrite <- FSuccSimpl1; auto. apply FSuccCanonic; auto. intros H'5; apply Rlt_le. unfold FtoRradix in |- *; apply FcanonicPosFexpRlt with (3 := pGivesBound); auto. apply Rle_trans with (r2 := FtoR radix x); auto. apply Rlt_le; auto. apply FSuccLt; auto. apply Rle_trans with (r2 := FtoR radix x); auto with real. apply FSuccCanonic; auto. rewrite FSuccSimpl4; auto. apply sym_not_equal; apply Z.lt_neq. apply Z.lt_le_trans with (m := 0%Z); auto with zarith. replace 0%Z with (- 0)%Z; auto with zarith. apply Zlt_Zopp. apply nNormPos; auto. apply LeR0Fnum with (radix := radix); auto with zarith. intros H'4; elim H'4; intros H'5 H'6; clear H'4. generalize (Z_eq_bool_correct (Fnum x) (Zpos (vNum b))); case (Z_eq_bool (Fnum x) (Zpos (vNum b))); intros H'4. contradict H'6; auto. apply Zle_not_lt; apply Zlt_le_weak. rewrite H'4; auto with zarith. rewrite <- (Z.abs_eq (Fnum y)); auto with zarith; try apply Fb1. apply LeR0Fnum with (radix := radix); auto with zarith. apply Rle_trans with (FtoRradix x); auto with real. case (Zlt_next _ _ H'6); intros H'7. rewrite FSuccSimpl4; auto. rewrite <- H'7; rewrite H'5; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real. apply Z.lt_neq. unfold pPred in |- *; apply Zlt_succ_pred; rewrite <- H'7; auto with zarith. rewrite <- (Z.abs_eq (Fnum y)); auto with zarith; try apply Fb1. apply LeR0Fnum with (radix := radix); auto with zarith. apply Rle_trans with (FtoRradix x); auto with real. apply Zlt_not_eq_rev. apply Z.lt_le_trans with (m := 0%Z); auto with zarith. replace 0%Z with (- 0)%Z; auto with zarith. apply Zlt_Zopp. apply nNormPos; auto. apply LeR0Fnum with (radix := radix); auto with zarith. rewrite FSuccSimpl4; auto. replace y with (Float (Fnum y) (Fexp y)). rewrite H'5. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; auto with zarith. apply IZR_le; auto with zarith. case y; simpl in |- *; auto. contradict H'7; auto. apply Zle_not_lt; apply Zlt_le_weak. rewrite H'7. unfold pPred in |- *; rewrite <- Zsucc_pred. rewrite <- (Z.abs_eq (Fnum y)); try apply Fb1. apply LeR0Fnum with (radix := radix); auto with zarith. apply Rle_trans with (FtoRradix x); auto with real. apply Zlt_not_eq_rev. apply Z.lt_le_trans with (m := 0%Z); auto with zarith. replace 0%Z with (- 0)%Z; auto with zarith. apply Zlt_Zopp. apply nNormPos; auto. apply LeR0Fnum with (radix := radix); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz