fact: Definition lens (G : graph2) := [&& edge_set G (@bag G IO input) == set0 , edge_set G (@bag G IO output) == set0 & @link_rel (skeleton G) input output].
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)