proposition: Lemma find_min_lt_inf: forall u l, u = find l (fold_right Z.min (hd 0 l) l) 0 -> (@isEmpty inf l) = Vzero -> Zlength l > 0 -> Znth u l < inf + 1.
proof: Proof. intros. rewrite <- isEmpty_in' in H0. destruct H0 as [? [? ?]]. rewrite H. rewrite Znth_find. - pose proof (fold_min _ _ H0). lia. - now apply fold_min_in_list. Qed.
imports: CertiGraph.prim.prim_env CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceUAdjMatGraph1 CertiGraph.prim.prim_spec1