fact: Definition inv_unpopped (g : @DijkGG size inf) src (popped prev: list V) (dist: list Z) (dst: V) := ~ In dst popped -> Znth dst dist < inf -> dst = src \/ (dst <> src /\ let mom := Znth dst prev in vvalid g mom /\ In mom popped /\ elabel g (mom, dst) < inf /\ Znth mom dist + elabel g (mom, dst) < inf /\ Znth dst dist = Znth mom dist + elabel g (mom, dst) /\ forall mom', vvalid g mom' -> In mom' popped -> Znth dst dist <= Znth mom' dist + elabel g (mom', dst)).
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph