∀ (limit count : ℕ) (iter : ByteArray.Iterator),
  ¬count ≥ limit →
    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun count iter => limit - count) ⟨count + 1, iter.next⟩
      ⟨count, iter⟩