proposition: Theorem digitVNumiSPrecision : digit radix (Zpos (vNum b)) = S precision.
proof: Proof. apply digitInv; auto. rewrite pGivesBound. rewrite Z.abs_eq; try lia. auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz