proposition: Lemma iso_Lovasz_const1 (G : sgraph) (m : G -> nat) : (forall x : G, m x = 1) -> G ≃ Lovasz m.
proof: Proof. move => ?; have M1 : m =1 fun=> 1 by []. apply: diso_comp (iso_Lovasz1 G) _. exact/diso_sym/eq_iso_Lovasz. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)