proposition: Theorem Konig (G : sgraph) (A V : {set G}) (M : {set {set G}}) : bipartition A -> smallest vcover V -> largest matching M -> #|V| = #|M|.
proof: Proof. move => bip_A [cov_V min_V] [match_M max_M]. apply/eqP. rewrite eqn_leq cover_matching // andbT. case: (min_vcover_matching (V := V) bip_A _) => // M' H ->. exact: max_M. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)