proposition: Lemma remove_loops (G : graph) (E : {set edge G}) : {in E, forall e, source e = target e} -> diso G (remove_edges E).
proof: Proof. move=> Eloops. have Esame x y : x != y -> @edges _ _ (remove_edges E) x y = val @^-1: @edges _ _ G x y. { move=> xNy. apply/setP=> e. by rewrite !inE. } exists (bij_id: bij G (remove_edges E)) => //= x y; rewrite /=/sk_rel => /andP[xNy]. all: rewrite /edge_rel/=/sk_rel. all: rewrite xNy /adjacent/= !Esame // 1?eq_sym // -preimsetU. - case/existsP=> e He. suff H : e \notin E by apply/existsP; exists (Sub e H); rewrite inE. apply: contraNN xNy => /Eloops eq_e. move: He. rewrite !inE -eq_e. by case/orP=> /andP[/eqP<- /eqP<-]. - case/existsP=> e. rewrite inE => He. apply/existsP. by exists (val e). 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)