∀ (n : ℕ),
  Disjoint
    (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))))
      n.divisorsAntidiagonal)
    (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding)
      n.divisorsAntidiagonal)