Graph theory def: Maximal/maximum matchings

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, including:

/-- A maximum matching is a maximal matching. -/
theorem IsMaximumMatching.isMaximalMatching {M : G.Subgraph} (hfin : M.edgeSet.Finite)
    (h : M.IsMaximumMatching) : M.IsMaximalMatching := by
  refine h.maximal_of_strictMonoOn <| mk_strictMonoOn.comp IsMatching.strictMonoOn_edgeSet ?_
  exact fun _ h' ↦ hfin.finite_of_encard_le <| toENat.monotone' <| h.le h'

/-- A perfect matching is a maximum matching. -/
theorem IsPerfectMatching.isMaximumMatching {M : G.Subgraph} (h : M.IsPerfectMatching) :
    M.IsMaximumMatching := sorry

/-- A perfect matching is a maximal matching. -/
theorem IsPerfectMatching.isMaximalMatching {M : G.Subgraph} (h : M.IsPerfectMatching) :
    M.IsMaximalMatching := sorry

Start by reading the existing SimpleGraph.Subgraph.IsMatching definition and API in Mathlib/Combinatorics/SimpleGraph/Matching.html. Define the proposed maximal and maximum predicates, then use the stated theorem signatures to guide the API, including the relationships with finite and perfect matchings. Done means the definitions and basic lemmas are added with proofs rather than sorry.