proposition: Lemma MaxRlist_P1 : forall (l:list R) (x:R), In x l -> x <= MaxRlist l.
proof: Proof. intros; induction l as [| r l Hrecl]. - simpl in H; elim H. - induction l as [| r0 l Hrecl0]. + simpl in H; elim H; intro. * simpl; right; symmetry; assumption. * elim H0. + replace (MaxRlist (r :: r0 :: l)) with (Rmax r (MaxRlist (r0 :: l))). * simpl in H; decompose [or] H. -- rewrite H0; apply RmaxLess1. -- unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. ++ apply Hrecl; simpl; tauto. ++ apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. -- unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. ++ apply Hrecl; simpl; tauto. ++ apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. * reflexivity. Qed.
imports: List Rbase Rfunctions