proposition: Lemma CK4F_remove_loops (G : graph2) (E : {set edge G}) : CK4F G -> input == output :> G -> E \subset edge_set IO -> CK4F (point (remove_edges E) input output).
proof: Proof. move=> [G_conn G_CK4F] /eqP Eio E_sub_IO. rewrite -Eio. have loopP : {in E, forall e, source e = target e}. { move => e /(subsetP E_sub_IO). rewrite !inE. case/andP. by do 2 case/orP=> [/eqP->|/eqP->]. } split. - apply: iso_connected G_conn. symmetry. exact: remove_loops. - apply: iso_K4_free G_CK4F. apply: diso_comp (iso_pointxx _) _. case: G {G_conn E_sub_IO} E Eio loopP => G i o E /= <- loopP. symmetry. apply: diso_comp (iso_pointxx _) _. exact: remove_loops. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)