proposition: Lemma RList_P17 : forall (l1:list R) (x:R) (i:nat), ordered_Rlist l1 -> In x l1 -> pos_Rl l1 i < x -> (i < pred (length l1))%nat -> pos_Rl l1 (S i) <= x.
proof: Proof. induction l1 as [ | r r0 H]. - intros; elim H0. - intros; induction i as [| i Hreci]. + simpl; elim H1; intro; [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2) | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ]. + simpl; simpl in H2; elim H1; intro. * rewrite <- H4 in H2; assert (H5 : r <= pos_Rl r0 i); [ apply Rle_trans with (pos_Rl r0 0); [ apply (H0 0%nat); simpl; simpl in H3; apply Nat.neq_0_lt_0; red; intro; rewrite H5 in H3; elim (Nat.nlt_0_r _ H3) | elim (RList_P6 r0); intros; apply H5; [ apply RList_P4 with r; assumption | apply Nat.le_0_l | simpl in H3; apply Nat.succ_lt_mono; apply Nat.lt_trans with (length r0); [ apply H3 | apply Nat.lt_succ_diag_r ] ] ] | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H2)) ]. * apply H; try assumption; [ apply RList_P4 with r; assumption | simpl in H3; apply Nat.succ_lt_mono; replace (S (pred (length r0))) with (length r0); [ apply H3 | symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H5 in H3; elim (Nat.nlt_0_r _ H3) ] ]. Qed.
imports: List Rbase Rfunctions