Function next_day 

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

requires

datetime_wf(value),

ensures

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

returns

nxt_dy!(value),