proposition: Lemma edge_cost_pos: forall (g: DijkGG) e, 0 <= elabel g e.
proof: Proof. intros. pose proof (valid_edge_bounds g e). pose proof (invalid_edge_weight g e). destruct (@evalid_dec _ _ _ _ g (finGraph g) e). - apply H; trivial. - rewrite H0 in n. replace (elabel g e) with inf by trivial. pose proof (@inf_representable _ _ g). lia. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph