∀ {n : ℕ} (c : OrderedFinpartition (n + 1)) (x : Fin n) (j : Fin (c.partSize (c.index 0))),
  ↑j ≠ 0 →
    c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0) →
      Function.update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) = c.partSize (c.index 0) - 1 →
        ¬↑j - 1 + 1 = ↑j → False