proposition: Lemma expand_loop (G : pre_graph) (isG : is_graph G) (x : VT) (e : ET) u : is_edge G e x u x -> pack G ≃2 pack (G - [fset e]) ∔ [pack_v x, le G e, pack_v x].
proof: Proof. move => edge_e. symmetry. have E : (G - [fset e]) ∔ [e,x,le G e,x] ≡G G. { rewrite remove_edgeK //. by case: edge_e => E [A B C]. } apply: iso2_comp (iso2_sym _) _. unshelve eapply (pack_add_edge' (G := G - [fset e]) (e := e)). { symmetry in E. apply: eqvG_graph E. } - by rewrite /= !inE eqxx. - exact: eqvG_pack E. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)