proposition: Lemma always_room_for_inf: 0 < size <= Int.max_signed -> 0 <= (Int.max_signed / size) * (size - 1) < Int.max_signed.
proof: Proof. intros. remember Int.max_signed as m. split. apply Z.mul_nonneg_nonneg. apply Z.div_pos. 1,2,3: lia. pose proof (Z.mul_div_le m size). spec H0. lia. rewrite Z.mul_sub_distr_l, Z.mul_1_r. pose proof (edges_can_be_positive). subst m. lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph