proposition: Lemma strong_evalid_dijk: forall (g: DijkGG) a b, vvalid g a -> vvalid g b -> elabel g (a, b) <> inf -> strong_evalid g (a,b).
proof: Proof. intros. split3; [rewrite (evalid_meaning g) | rewrite (edge_src_fst g) | rewrite (edge_dst_snd g)]; trivial. split; trivial. apply edge_representable. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph