proposition: Lemma in_lmin : forall x l, In x l -> lmin l <= x.
proof: Proof. induction l; simpl; intro. contr. destruct H. subst a. apply Nat.le_min_l. ded (IHl H). apply elim_min_r. exact H0. Qed.
imports: CoLoR(ListUtil LogicUtil NatUtil)