fact: Definition src_picked_first h src (popped: list V) := 0 < Zlength (heap_items h) -> popped = [] -> forall min_item, In min_item (heap_items h) -> Forall (cmp_rel min_item) (heap_items h) -> src = Int.signed (heap_item_payload min_item).
imports: CertiGraph.graph.SpaceAdjMatGraph2 CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_math_proof CertiGraph.dijkstra.dijkstra_spec2 CertiGraph.dijkstra.dijkstra_constants