proposition: Lemma Znth_dist_cases: forall i dist, 0 <= i < Zlength dist -> inrange_dist dist -> Znth i dist = inf \/ 0 <= Znth i dist <= (size - 1) * (Int.max_signed / size).
proof: Proof. intros. apply (sublist.Forall_Znth _ _ _ H) in H0. ulia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure