proposition: Lemma iso_iso2 (F G: graph) (h: F ≃ G) (i o: F): point F i o ≃2 point G (h i) (h o).
proof: Proof. now exists h. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)