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