proposition: Lemma adjacent_induced (G : graph) (V : {set G}) (x y : induced V) : adjacent x y = adjacent (val x) (val y).
proof: Proof. apply/existsP/existsP => -[e]; rewrite ?inE => He. - exists (val e). move: He. by rewrite !inE -!val_eqE. - suff eV : e \in edge_set V by exists (Sub e eV); rewrite !inE -!val_eqE. rewrite inE. case/orP: He => /andP[/eqP-> /eqP->]; apply/andP; split; exact: valP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)