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