proposition: Lemma path_cost_pos: forall (g: DijkGG) p, valid_path g p -> 0 <= path_cost g p.
proof: Proof. intros. apply acc_pos; [|Lia.lia]. intros. apply edge_cost_pos. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph