proposition: Theorem maxFbounded : forall (b : Fbound) (z : Z), (- dExp b <= z)%Z -> Fbounded b (Float (Z.pred (Zpos (vNum b))) z).
proof: Proof. intros b z H; split; auto. change (Z.abs (Z.pred (Zpos (vNum b))) < Zpos (vNum b))%Z in |- *. rewrite Z.abs_eq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz