proposition: Lemma RList_P4 : forall (l1:list R) (a:R), ordered_Rlist (a :: l1) -> ordered_Rlist l1.
proof: Proof. intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl; replace (length l1) with (S (pred (length l1))); [ apply -> Nat.succ_lt_mono; assumption | apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H1 in H0; elim (Nat.nlt_0_r _ H0) ]. Qed.
imports: List Rbase Rfunctions