∀ (s₁ s₂ : String.Legacy.Iterator),
  String.ltb s₁ s₂ =
    if s₂.hasNext = true then
      if s₁.hasNext = true then if s₁.curr = s₂.curr then String.ltb s₁.next s₂.next else decide (s₁.curr < s₂.curr)
      else true
    else false