proposition: Theorem FulpSucCan : forall p : float, Fcanonic radix b p -> (FSucc b radix precision p - p <= Fulp p)%R.
proof: Proof. intros p H'. replace (Fulp p) with (powerRZ radix (Fexp p)). 2: unfold Fulp in |- *; replace (Fnormalize radix b precision p) with p; auto; apply sym_equal; apply FcanonicUnique with (3 := pGivesBound); auto with arith; try apply FnormalizeCanonic; auto with zarith. 2: apply FcanonicBound with (1 := H'); auto with zarith. 2: apply FnormalizeCorrect; easy. unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with zarith. case (Z.eq_dec (Fnum p) (- nNormMin radix precision)); intros H1'. case (Z.eq_dec (Fexp p) (- dExp b)); intros H2'. rewrite FSuccDiff2; auto with arith. unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real. rewrite FSuccDiff3; auto with arith zarith. unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l. apply Rlt_le; apply Rlt_powerRZ; try apply IZR_lt; auto with real zarith. unfold Z.pred in |- *; auto with zarith. rewrite FSuccDiff1; auto with arith zarith. unfold FtoR in |- *; simpl in |- *; rewrite Rmult_1_l; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz