proposition: Theorem FboundedZeroSameExp : forall (b : Fbound) (p : float), Fbounded b p -> Fbounded b (Fzero (Fexp p)).
proof: Proof. intros b p H'; (repeat split; simpl in |- *; auto with zarith). apply H'. Qed.
imports: Reals ZArith List PeanoNat Psatz