proposition: Theorem FboundedFzero : forall b : Fbound, Fbounded b (Fzero (- dExp b)).
proof: Proof. intros b; repeat (split; simpl in |- *). replace 0%Z with (- 0)%Z; [ idtac | simpl in |- *; auto ]. apply Zeq_le; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz