mathlib

edfe7e1e - feat(combinatorics/simple_graph): degree lemmas (#5966)

feat(combinatorics/simple_graph): degree lemmas (#5966) Proves some lemmas about the minimum/maximum degree of vertices in a graph - also weakens the assumptions for the definitions, following the usual mathlib pattern of defining total functions.