proposition: Lemma RList_P6 : forall l:list R, ordered_Rlist l <-> (forall i j:nat, (i <= j)%nat -> (j < length l)%nat -> pos_Rl l i <= pos_Rl l j).
proof: Proof. induction l as [ | r r0 H]; split; intro. - intros; right; reflexivity. - unfold ordered_Rlist;intros; simpl in H0; elim (Nat.nlt_0_r _ H0). - intros; induction i as [| i Hreci]; [ induction j as [| j Hrecj]; [ right; reflexivity | simpl; apply Rle_trans with (pos_Rl r0 0); [ apply (H0 0%nat); simpl; simpl in H2; apply Nat.neq_0_lt_0; red; intro; rewrite H3 in H2; assert (H4 := proj2 (Nat.succ_lt_mono _ _) H2); elim (Nat.nlt_0_r _ H4) | elim H; intros; apply H3; [ apply RList_P4 with r; assumption | apply Nat.le_0_l | simpl in H2; apply Nat.succ_lt_mono; assumption ] ] ] | induction j as [| j Hrecj]; [ elim (Nat.nle_succ_0 _ H1) | simpl; elim H; intros; apply H3; [ apply RList_P4 with r; assumption | apply le_S_n; assumption | simpl in H2; apply Nat.succ_lt_mono; assumption ] ] ]. - unfold ordered_Rlist; intros; apply H0; [ apply Nat.le_succ_diag_r | simpl; simpl in H1; apply -> Nat.succ_lt_mono; assumption ]. Qed.
imports: List Rbase Rfunctions