proposition: Lemma minlist_smaller : forall l x, member x l -> minlist l [<=] x.
proof: Proof. intros l x H. induction l as [| a l Hrecl]. easy. simpl in |- *. astepl match l with | nil => a | cons _ _ => Min a (minlist l) end. induction l as [| a0 l Hrecl0]. simpl in H; elim H. intro; tauto. intro; cut (a [=] x); [ apply eq_imp_leEq | apply eq_symmetric_unfolded; assumption ]. simpl in H. elim H. intro. apply leEq_transitive with (minlist (cons a0 l)). apply Min_leEq_rht. apply Hrecl; assumption. intro; astepr a; apply Min_leEq_lft. Qed.
imports: CoRN.reals.CReals1