sorry ↔ ∃ f, Set.InjOn (fun x => match x with | (a, b) => Polynomial.eval (↑a) f + Polynomial.eval (↑b) f) {(a, b) | a < b}