proposition: Lemma cliqueb_isubgraph (K : {set F}) : cliqueb K = cliqueb (i @: K).
proof: Proof. rewrite /cliqueb (@forall2_imset _ _ i i). apply: eq_forall_in => x xK; apply: eq_forall_in => y yK. by rewrite (inj_eq (isubgraph_inj i)) isubgraph_mono. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)