proposition: Lemma omega_isubgraph (B : {set F}) : ω(B) = ω(i @: B).
proof: Proof. apply/eqP; rewrite eqn_leq; apply/andP; split. - have [K] := omegaP B. rewrite inE isubgraph_cliques => /andP[ckK _]; rewrite -(card_imset _ i_inj). exact: clique_bound. - have [K] := omegaP; rewrite inE => /andP[clK]. move/clique_to_isubgraph : (clK). rewrite can_inj_imset => clK' _. apply: leq_trans (clique_bound clK'). rewrite inj_card_preimset //. exact: subset_trans (cliques_subset clK) (imset_codom _ _). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)