fact: Fixpoint insert (g:EdgeListGG) (i:EType) (l: list EType) := match l with | nil => i::nil | h::t => if (elabel g i <=? elabel g h) then i::h::t else h :: insert g i t end.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph