proposition: Lemma RList_P25 : forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> pos_Rl l1 (pred (length l1)) <= pos_Rl l2 0 -> ordered_Rlist (app l1 l2).
proof: Proof. induction l1 as [ | r r0 H]. - intros; simpl; assumption. - induction r0 as [ | r1 r2 H0]. + intros; simpl; simpl in H2; unfold ordered_Rlist; intros; simpl in H3. induction i as [| i Hreci]. * simpl; assumption. * change (pos_Rl l2 i <= pos_Rl l2 (S i)); apply (H1 i); apply Nat.succ_lt_mono; replace (S (pred (length l2))) with (length l2); [ assumption | symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H4 in H3; elim (Nat.nlt_0_r _ H3) ]. + intros; assert (H4 : ordered_Rlist (app (r1 :: r2) l2)). * apply H; try assumption. apply RList_P4 with r; assumption. * unfold ordered_Rlist; intros i H5; simpl in H5. induction i as [| i Hreci]. -- simpl; apply (H1 0%nat); simpl; apply Nat.lt_0_succ. -- change (pos_Rl (app (r1 :: r2) l2) i <= pos_Rl (app (r1 :: r2) l2) (S i)); apply (H4 i); simpl; apply Nat.succ_lt_mono; assumption. Qed.
imports: List Rbase Rfunctions