proposition: Theorem FSuccLt : forall a : float, (a < FSucc a)%R.
proof: Proof. intros a; 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'; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H'. unfold pPred in |- *; rewrite (PosNormMin radix) with (precision := precision); auto with zarith; unfold nNormMin in |- *. rewrite powerRZ_Zs; auto with real zarith. 2: apply Rgt_not_eq, IZR_lt; lia. repeat rewrite <- Rmult_assoc. apply Rlt_monotony_exp; auto with zarith. rewrite Zmult_comm. rewrite <- mult_IZR. apply IZR_lt; auto with zarith. intros H'; generalize (Z_eq_bool_correct (Fnum a) (- nNormMin radix precision)); case (Z_eq_bool (Fnum a) (- nNormMin radix precision)). intros H'0; generalize (Z_eq_bool_correct (Fexp a) (- dExp b)); case (Z_eq_bool (Fexp a) (- dExp b)). intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *. apply Rlt_monotony_exp; auto with real zarith. apply IZR_lt; auto with zarith. intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *; rewrite H'0. pattern (Fexp a) at 1 in |- *; replace (Fexp a) with (Z.succ (Z.pred (Fexp a))). rewrite powerRZ_Zs. repeat rewrite <- Rmult_assoc. apply Rlt_monotony_exp; auto with real zarith. rewrite <- mult_IZR. apply IZR_lt; auto with zarith. rewrite <- Zopp_mult_distr_l. apply Zlt_Zopp. rewrite Zmult_comm. unfold pPred in |- *; rewrite (PosNormMin radix) with (precision := precision); auto with zarith. apply Rgt_not_eq, IZR_lt; lia. apply sym_equal; apply Zsucc_pred. intros H'1; unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real zarith. apply Rmult_lt_compat_r. apply powerRZ_lt, IZR_lt; auto with zarith. apply IZR_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz