proposition: Lemma not_in_popped_popped_short: forall (g: @DijkGG size inf) i popped, vvalid g i -> NoDup popped -> inrange_popped popped -> ~ In i popped -> Zlength popped <= size - 1.
proof: Proof. intros. apply (vvalid_meaning g) in H. apply (NoDup_all_bounded_Zlength' i); trivial. intros. split. - red in H1. rewrite Forall_forall in H1. apply H1; trivial. - intro. subst j; contradiction. Qed.
imports: CertiGraph.dijkstra.dijkstra_env CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure