proposition: Lemma Zlength_epath_to_vpath: forall A B (EV : EqDec A eq) (EE : EqDec B eq) (g : PreGraph A B) s l, Zlength (epath_to_vpath g (s,l)) = 1 + Zlength l.
proof: Proof. intros. simpl. assert (forall l, l <> [] -> Zlength (epath_to_vpath' g l) = 1 + Zlength l). { clear. induction l. contradiction. intros _. simpl. destruct l. reflexivity. rewrite Zlength_cons. rewrite IHl. 2: discriminate. repeat rewrite Zlength_cons. lia. } destruct l. reflexivity. rewrite H. reflexivity. discriminate. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.graph.MathAdjMatGraph