proposition: Lemma isubgraph_Lovasz (G : sgraph) (m' m : G -> nat) : (forall x, m' x <= m x) -> Lovasz m' ⇀ Lovasz m.
proof: Proof. move => leqM. pose f (u : Lovasz m') : Lovasz m := let: ⟨ x , i ⟩ := u in ⟨ x , widen_ord (leqM x) i ⟩. have inj_f : injective f. { move => [x i] [y j] /eqP E; apply/eqP; move: E. rewrite /f -!tag_eqE/tag_eq/=; case: (eqVneq x y) => //= xEy. by move: j; subst y => j; rewrite !tagged_asE -ord_eq /=. } have homo_f : {mono f : x y / x -- y}. { move => [x i] [y]; rewrite /f/edge_rel/=/LovaszRel/=. have [-> j|//] := eqVneq y x. by rewrite -!tag_eqE/tag_eq/= !tagged_asE -ord_eq /=. } exact: ISubgraph inj_f homo_f. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)