Graph theory def: Maximal/maximum matchings

[SnirBroshi]

Matchings in simple graphs exist as SimpleGraph.Subgraph.IsMatching.

I suggest we're missing the following defs for maximal matchings and maximum matchings:

open Cardinal

def Subgraph.IsMaximalMatching (M : G.Subgraph) : Prop :=
  Maximal IsMatching M

def Subgraph.IsMaximumMatching (M : G.Subgraph) : Prop :=
  MaximalFor IsMatching (#·.edgeSet) M

and basic API for them.

[SnirBroshi]

#32555