proposition: Theorem FBoundedPred : forall f : float, Fbounded b f -> Fbounded b (FPred f).
proof: Proof. intros f H'; rewrite (FPredFopFSucc f); auto with zarith. apply oppBounded, FBoundedSuc; try easy. now apply oppBounded. Qed.
imports: Reals ZArith List PeanoNat Psatz