proposition: Lemma less_minlist : forall x l, 0 < length l -> (forall y, member y l -> x [<] y) -> x [<] minlist l.
proof: Proof. simple induction l. simpl in |- *; intros; exfalso; inversion H. clear l. do 2 intro. intro H. clear H; induction l as [| a0 l Hrecl]. simpl in |- *; intros H H0. apply H0; right; algebra. generalize l a0 Hrecl; clear Hrecl l a0. intros l b; intros. rename X into H0. eapply less_wdr. 2: apply minlist_aux. astepr (Min b (minlist (cons a l))). apply less_Min. apply H0; left; right; algebra. apply Hrecl. simpl in |- *; auto with arith. intros y H1; apply H0. inversion_clear H1. left; left; assumption. right; assumption. Qed.
imports: CoRN.reals.CReals1