proposition: Lemma RList_P5 : forall (l:list R) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x.
proof: Proof. intros; induction l as [| r l Hrecl]; [ elim H0 | simpl; elim H0; intro; [ rewrite H1; right; reflexivity | apply Rle_trans with (pos_Rl l 0); [ apply (H 0%nat); simpl; induction l as [| r0 l Hrecl0]; [ elim H1 | simpl; apply Nat.lt_0_succ ] | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ]. Qed.
imports: List Rbase Rfunctions