proposition: Lemma card_maxclique K H : K \in maxcliques H -> #|K| = ω(H).
proof: Proof. rewrite inE => /andP[clK ltK]; apply/eqP; rewrite eqn_leq ltK andbT. exact: clique_bound. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)