proposition: Lemma always_room_for_inf': 0 < size * 4 <= Int.max_signed -> 0 <= (Int.max_signed / size) * (size - 1) < Int.max_signed.
proof: Proof. intros. apply always_room_for_inf. lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph