Function generalized_time_fraction 

pub open spec fn generalized_time_fraction(value: GeneralizedTimeSpec) -> Seq<u8>

{ if value.fraction.len() == 0 { Seq::empty() } else { seq![0x2eu8] + value.fraction } }