mathlib

f82572d6 - put vertex and edge types outside structure. this seems like a good idea. getting the opposite of an edge from a vertex is still noncomputable, though