proposition: Lemma popped_noninf_has_path: forall (g: @DijkGG size inf) mom src popped prev (dist: list Z), dijkstra_correct g src popped prev dist -> In mom popped -> Znth mom dist < inf -> vvalid g mom -> exists p2mom : path, path_correct g prev dist src mom p2mom /\ (forall step : Z, In_path g step p2mom -> In step popped) /\ path_globally_optimal g src mom p2mom.
proof: Proof. intros. destruct (H _ H2) as [? _]. specialize (H3 H0). destruct H3; [lia|]. apply H3; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure