mathlib3

e824f925 - tried a graph definition that is a fusion of hedetniemi and chou, but can't define function that gives vertex opposite an edge