naming conventions

Stream: graph theory

[Alena Gusakov]

How do we feel about referring to the cardinality of the vertex fintype as card_verts? e.g.

lemma card_common_neighbors_lt_card_verts (v w : V) :
  fintype.card (G.common_neighbors v w) < fintype.card V

[Alena Gusakov]

We already have

lemma degree_lt_card_verts (G : simple_graph V) (v : V) : G.degree v < fintype.card V

but I think that might've been from another one of my PRs. Can totally change it if anyone doesn't like it

[Bryan Gin-ge Chen]

I think that's fine. It's worth documenting conventions like this in module docstrings.