Function previous_day 

pub exec fn previous_day(value: DateTime) -> res : Option<DateTime>

requires

datetime_wf(value),

ensures

res matches Some(previous) ==> datetime_wf(previous),

returns

prev_dy!(value),