fact: Definition inrange_dist dist := Forall (fun x => 0 <= x <= (size - 1) * (Int.max_signed / size) \/ x = inf) dist.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure