proposition: Lemma path_in_popped_path_glue: forall (g: @DijkGG size inf) p1 p2 popped, path_in_popped g popped p1 -> path_in_popped g popped p2 -> path_in_popped g popped (path_glue p1 p2).
proof: Proof. red. intros. apply In_path_glue in H1. destruct H1. - apply H; trivial. - apply H0; trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure