∀ {p q : Polynomial ℤ} {k m m' n : ℕ},
  k < m →
    m < n →
      k < m' →
        m' < n →
          ∀ (u v w : ℤˣ),
            p = Polynomial.trinomial k m n ↑u ↑v ↑w →
              q = Polynomial.trinomial k m' n ↑u ↑v ↑w → p * p.mirror = q * q.mirror → q = p ∨ q = p.mirror