proposition: Theorem diHall (G : diGraph) A : bipartition A -> (forall S : {set G}, S \subset A -> #|S| <= #|NS(S)|) -> exists M, dimatching M /\ A = [set x.1 | x in M].
proof: Proof. move => bip_A N_A. have sep_A S : separator G A (~:A) S -> #|A| <= #|S|. { move => sep_S. rewrite -[#|A|](cardsID S). apply: (@leq_trans (#|A :&: S| + #|NS(A :\: S)|)). - by rewrite leq_add2l N_A // subsetDl. - rewrite -cardsUI [X in _ + X]eq_card0 ?addn0. + apply: subset_leq_card. rewrite subUset subsetIr /=. apply/subsetP => z /bigcupP [x /setDP[xA xNS]]; rewrite in_opn => xz. have [|s inS] := sep_S _ _ (edgep xz) xA; first by rewrite inE -(bip_A _ _ xz). rewrite mem_edgep => /pred2P [?|<- //]; subst; contrab. + move => z;rewrite !inE -andbA;apply/negbTE/negP. move => /and3P [zA zS /bigcupP [x /setDP [xA xS] xz]]. rewrite in_opn in xz. by rewrite (bip_A _ _ xz) zA in xA . } case: (Menger sep_A) => p con_p. clear sep_A bip_A. exists (dimatching_of p). split; first exact: connector_dimatching con_p. apply/setP => a. apply/idP/imsetP => [inA|[x]]. + move: (inj_card_onto_pred (f := fun i => fst (p i)) (P := (mem A))) => /=. case/(_ _ _ _ _ inA)/Wrap => //. * apply: fst_inj con_p. * apply: connector_fst con_p. * by rewrite card_ord. * case/mapP => i _ ->. exists (fst (p i),lst (p i)) => //. by rewrite imset_f. + case/imsetP => i _ -> /= ->. apply: connector_fst. exact: con_p. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)