proposition: Lemma RList_P2 : forall l1 l2:list R, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
proof: Proof. simple induction l1; [ intros; simpl; apply H | intros; simpl; apply H; apply RList_P1; assumption ]. Qed.
imports: List Rbase Rfunctions