proposition: Lemma MinRlist_P2 : forall l:list R, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l.
proof: Proof. intros; induction l as [| r l Hrecl]. - apply Rlt_0_1. - induction l as [| r0 l Hrecl0]. + simpl; apply H; simpl; tauto. + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). * unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. -- apply H; simpl; tauto. -- apply Hrecl; intros; apply H; simpl; simpl in H0; tauto. * reflexivity. Qed.
imports: List Rbase Rfunctions