proposition: Lemma eq_iso_Lovasz (G : sgraph) (m m' : G -> nat) : m =1 m' -> Lovasz m ≃ Lovasz m'.
proof: Proof. move => eq_m_m'; apply: isubgraph_iso. by apply: isubgraph_Lovasz => x; rewrite eq_m_m'. by rewrite !card_tagged !sumnE !big_map; apply: leq_sum => i; rewrite eq_m_m'. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)