proposition: Theorem FNSuccProp : forall x y : float, Fbounded b x -> Fbounded b y -> (x < y)%R -> (FNSucc x <= y)%R.
proof: Proof. intros x y H' H'0 H'1; unfold FNSucc in |- *. replace (FtoRradix y) with (FtoRradix (Fnormalize radix b precision y)). 2: unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. apply FSuccProp; auto with zarith. apply FnormalizeCanonic; easy. apply FnormalizeCanonic; easy. unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz