proposition: Lemma eqvG_graph (G H : pre_graph) (isG : is_graph G) : G ≡G H -> is_graph H.
proof: Proof. move => [EV EE Eep Elv Ele Ei Eo]. econstructor. - move => e b Ee. rewrite -EE in Ee. rewrite -EV -Eep //. exact: endptP. - rewrite -EV -Ei. exact: p_inP. - rewrite -EV -Eo. exact: p_outP. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)