simp_arith [LT.lt] at h
tag : Tag
time : Time.From tag.time
h : ¬tag.time < time.val
⊢ (increment tag).time = time.val
tag : Tag
time : Time.From tag.time
h : time.val.ns ≤ tag.time.ns
⊢ (increment tag).time = time.val