proposition: Lemma path_cost_path_glue_lt: forall (g: DijkGG) p1 p2 limit, valid_path g p1 -> valid_path g p2 -> path_cost g (path_glue p1 p2) < limit -> path_cost g p1 < limit /\ path_cost g p2 < limit.
proof: Proof. intros. rewrite (path_cost_path_glue g) in H1. pose proof (path_cost_pos _ _ H). pose proof (path_cost_pos _ _ H0). split; lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph