proposition: Lemma Closestbplusb: forall b0:Fbound, forall z:R, forall f:float, (Closest (plusExp b0) radix z f) -> (Fbounded b0 f) -> (Closest b0 radix z f).
proof: Proof. intros. split; auto. intros g Fg; elim H; intros. apply H2; auto. elim Fg; intros; split; unfold plusExp; auto. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; simpl; rewrite <- T; lia. intros;unfold Nplus. case x; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz