simp [LT.lt] at *
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }
tag : Tag
t : Time.From tag.time
h✝ : tag.time.ns < t.val.ns
⊢ if tag.time = t.val then tag.microstep < 0 else tag.time.ns < t.val.ns