proposition: Theorem oppBoundedInv : forall (b : Fbound) (x : float), Fbounded b (Fopp x) -> Fbounded b x.
proof: Proof. intros b x H'; rewrite <- (Fopp_Fopp x). apply oppBounded; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz