proposition: Lemma RList_P7 : forall (l:list R) (x:R), ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (length l)).
proof: Proof. intros; assert (H1 := RList_P6 l); elim H1; intros H2 _; assert (H3 := H2 H); clear H1 H2; assert (H1 := RList_P3 l x); elim H1; clear H1; intros; assert (H4 := H1 H0); elim H4; clear H4; intros; elim H4; clear H4; intros; rewrite H4; assert (H6 : length l = S (pred (length l))). - symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H6 in H5; elim (Nat.nlt_0_r _ H5). - apply H3; [ rewrite H6 in H5; apply Nat.lt_succ_r; assumption | apply Nat.lt_pred_l; red; intro; rewrite H7 in H5; elim (Nat.nlt_0_r _ H5) ]. Qed.
imports: List Rbase Rfunctions