The definition of service_at in ideal.v service_on in ideal.v is given using the implicit conversion nat_of_bool as s == Some j.
service_at
service_on
nat_of_bool
s == Some j
Unfolding this definition would give if s == Some j then 1 else 0 which should be equivalent and feels more readable.
if s == Some j then 1 else 0