proposition: Lemma iso_Lovasz1 (G : sgraph) : G ≃ Lovasz (fun _ : G => 1).
proof: Proof. set L := Lovasz _. pose f (x : G) : L := ⟨ x , ord0 ⟩. rewrite /= in f. pose g (x : L) : G := tag x. have can_f : cancel f g by []. have can_g : cancel g f. { move => [x n];apply/eqP; rewrite /f/g/= tagged_eq. exact/eqP/esym/fintype.ord1. } apply: (@Diso' G L) can_f can_g _ => x y. rewrite /f{1}/edge_rel/=/LovaszRel/=. by have [->|//] := eqVneq y x; rewrite tagged_eq eqxx sgP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)