proposition: Lemma MaxRlist_P2 : forall l:list R, (exists y : R, In y l) -> In (MaxRlist l) l.
proof: Proof. intros; induction l as [| r l Hrecl]. - simpl in H; elim H; trivial. - induction l as [| r0 l Hrecl0]. + simpl; left; reflexivity. + change (In (Rmax r (MaxRlist (r0 :: l))) (r :: r0 :: l)); unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. * right; apply Hrecl; exists r0; left; reflexivity. * left; reflexivity. Qed.
imports: List Rbase Rfunctions