proposition: Lemma fold_min_in_list: forall l, Zlength l > 0 -> In (fold_right Z.min (hd 0 l) l) l.
proof: Proof. intros. apply min_in_list. - apply incl_refl. - rewrite <- Znth_0_hd by trivial. apply Znth_In; lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext