proposition: Lemma inf_bounded_above_dist: forall (g: DijkGG), (size - 1) * (Int.max_signed / size) < inf.
proof: Proof. intros. pose proof (inf_further_restricted g). rewrite Z.mul_comm. trivial. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph