proposition: Theorem R0RltRleSucc : forall x : float, (x < 0)%R -> (FSucc x <= 0)%R.
proof: Proof. intros a H'; unfold FSucc in |- *. generalize (Z_eq_bool_correct (Fnum a) (pPred (vNum b))); case (Z_eq_bool (Fnum a) (pPred (vNum b))); auto. intros H'0; absurd (Fnum a < 0)%Z; auto. rewrite H'0; auto with zarith arith. apply Zle_not_lt; unfold pPred in |- *; apply Zle_Zpred; auto with zarith. apply R0LtFnum with (radix := radix); auto with zarith. generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)); intros H'1. generalize (Z_eq_bool_correct (Fexp a) (- dExp b)); case (Z_eq_bool (Fexp a) (- dExp b)); intros H'2. intros H'0. apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith. apply Zlt_le_succ. apply R0LtFnum with (radix := radix); auto with zarith. intros H'0. apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith. replace 0%Z with (- (0))%Z; [ apply Zle_Zopp | simpl in |- *; auto ]. unfold pPred in |- *; apply Zle_Zpred; apply Z.lt_trans with 1%Z; auto with zarith; apply (vNumbMoreThanOne radix) with (precision := precision); auto with zarith. intros H'0. apply LeZEROFnum with (radix := radix); simpl in |- *; auto with zarith. apply Zlt_le_succ. apply R0LtFnum with (radix := radix); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz