Dilworth's Theorem: in any partial ordering, the size of the largest possible antichain is equal to the smallest possible number of chains in a partition of the items into chains.

If you already know, in a bipartite graph with $$n$$ vertices, maximum matching $$M$$, and maximum independent set $$I$$, that $$n=|M|+|I|$$, then a proof is easy: form a bipartite graph with $$2n$$ vertices, one copy of each item of the ordering in each side and an edge from the smaller to the larger of each pair of comparable items. Find a matching $$M$$ and maximum independent set $$I$$. The edges of $$M$$ decompose the items into $$n-|M|$$ chains, and the items that have both of their copies belonging to $$I$$ form an antichain of at least $$n-|M|$$ items. The antichain must have exactly $$n-|M|$$ items, for it can have at most one item from each chain.

Anyway, I've now implemented all this in PADS. It's in a new module PartialOrder.py, which also contains everything that used to be in TopologicalOrder.py. Along with the new MaximumAntichain and MinimumChainDecomposition functions, I included a TransitiveClosure function, as it was needed when the input order is given by a sparser DAG.