proposition: Lemma evalid_dijk: forall (g: DijkGG) a b, 0 <= elabel g (a,b) < inf -> evalid g (a,b).
proof: Proof. intros. rewrite (evalid_meaning g); split. 1: apply edge_representable. intro. unfold AdjMatGG_DijkGG in H0. simpl in H0. lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph