monlib4

Formalising non-commutative graph theory in Lean 4.

Previous version: monlib in Lean 3