proposition: Lemma MinRlist_P1 : forall (l:list R) (x:R), In x l -> MinRlist l <= x.
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; assumption. * elim H0. + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). * simpl in H; decompose [or] H. -- rewrite H0; apply Rmin_l. -- unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. ++ apply Rle_trans with (MinRlist (r0 :: l)). ** assumption. ** apply Hrecl; simpl; tauto. ++ apply Hrecl; simpl; tauto. -- apply Rle_trans with (MinRlist (r0 :: l)). ++ apply Rmin_r. ++ apply Hrecl; simpl; tauto. * reflexivity. Qed.
imports: List Rbase Rfunctions