proposition: Lemma maxlist_greater : forall l x, member x l -> x [<=] maxlist l.
proof: Proof. intros l x H. induction l as [| a l Hrecl]. exfalso; assumption. simpl in |- *. induction l as [| a0 l Hrecl0]. simpl in H; elim H. intro; tauto. intro; apply eq_imp_leEq. auto. simpl in H. elim H. intro. apply leEq_transitive with (maxlist (cons a0 l)). apply Hrecl; assumption. apply rht_leEq_Max. intro; astepl a; apply lft_leEq_Max. Qed.
imports: CoRN.reals.CReals1