proposition: Lemma add_edgeV (G : pre_graph) e (x y : VT) (u : tm) : is_graph (add_edge' G e x u y) -> ((x \in vset G) * (y \in vset G))%type.
proof: Proof. intros graph_G. case: graph_G => /(_ e) H _ _. split. - move: (H false). rewrite endpt_add_edge. apply. by rewrite !inE eqxx. - move: (H true). rewrite endpt_add_edge. apply. by rewrite !inE eqxx. 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)