fact: Definition path_globally_optimal (g: @DijkGG size inf) src dst p : Prop := forall p', valid_path g p' -> path_ends g p' src dst -> path_cost g p <= path_cost g p'.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph