proposition: Theorem Hall (G : sgraph) A : bipartition A -> (forall S : {set G}, S \subset A -> #|S| <= #|NS(S)|) -> exists M, matching M /\ A \subset cover M.
proof: Proof. move => bip_A N_A. case: (@diHall G A) => [//|//|M' [M1 M2]]. - case: M1 => M1 M1'. exists (matching_of M'). split; first exact: matching_of_dimatching. rewrite M2. apply/subsetP => a. case/imsetP => e E1 E2. apply/bigcupP. exists [set e.1; e.2]; last by rewrite E2 !inE eqxx. exact: imset_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)