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