pub open spec fn der_real_decimal_wf(bytes: Seq<u8>) -> bool
{ exists |dot: int| der_real_decimal_at(bytes, dot) }