Function ascii_digits_have_nonzero 

pub open spec fn ascii_digits_have_nonzero(bytes: Seq<u8>, start: int, end: int) -> bool

{ exists |i: int| start <= i < end && ascii_nonzero_digit(bytes[i]) }