mathlib3

f070401d - the standard simplex has an extra degeneracy