proposition: Lemma edge_representable: forall (g: DijkGG) e, Int.min_signed <= elabel g e <= Int.max_signed.
proof: Proof. intros. pose proof (valid_edge_bounds g e). pose proof (invalid_edge_weight g e). pose proof (edge_cost_pos g e). destruct (@evalid_dec _ _ _ _ g (finGraph g) e). - specialize (H e0). split; trivial. rep_lia. apply Z.le_trans with (m := (Int.max_signed / size)). apply H. pose proof (size_representable g). apply Z.le_trans with (m := Int.max_signed / size). lia. etransitivity. apply div_pos_le; lia. lia. - rewrite H0 in n. replace (elabel g e) with inf by trivial. pose proof (inf_representable g). split; rep_lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph