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