proposition: Lemma min_in_list : forall l1 l2 starter, incl l1 l2 -> In starter l2 -> In (fold_right Z.min starter l1) l2.
proof: Proof. intros. induction l1; trivial. simpl. destruct (Z.min_dec a (fold_right Z.min starter l1)); rewrite e; clear e. apply H, in_eq. apply IHl1, (incl_cons_inv H). Qed.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext