proposition: Lemma min_not_in_prev i l : Znth i l < fold_right Z.min (Znth 0 l) (sublist 0 i l) -> ~ In (Znth i l) (sublist 0 i l).
proof: Proof. intros. intro. pose proof (fold_min_general (sublist 0 i l) (Znth i l) H0(Znth 0 l)). lia. Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext