∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj (SimplexCategory.mk p))
          (SSet.stdSimplex.obj (SimplexCategory.mk q))).obj
      (Opposite.op (SimplexCategory.mk n)))
  {m : ℕ} (hm : p + q = m),
  StrictMono ⇑(SSet.prodStdSimplex.orderHomOfSimplex x hm) ↔ StrictMono ⇑(SSet.prodStdSimplex.objEquiv x)