proposition: Theorem vNumPrecision : forall n : Z, digit radix n <= precision -> (Z.abs n < Zpos (vNum b))%Z.
proof: Proof. intros n H'. rewrite <- (Z.abs_eq (Zpos (vNum b))); auto with zarith. apply digit_anti_monotone_lt with (n := radix); auto. rewrite digitVNumiSPrecision; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz