proposition: Theorem oppBounded : forall (b : Fbound) (x : float), Fbounded b x -> Fbounded b (Fopp x).
proof: Proof. intros b x H'; repeat split; simpl in |- *; auto with zarith. replace (Z.abs (- Fnum x)) with (Z.abs (Fnum x)); try apply H'. case (Fnum x); simpl in |- *; auto. apply H'. Qed.
imports: Reals ZArith List PeanoNat Psatz