proposition: Lemma RList_P26 : forall (l1 l2:list R) (i:nat), (i < length l1)%nat -> pos_Rl (app l1 l2) i = pos_Rl l1 i.
proof: Proof. simple induction l1. - intros; elim (Nat.nlt_0_r _ H). - intros; induction i as [| i Hreci]. + apply RList_P22; discriminate. + apply (H l2 i); simpl in H0; apply Nat.succ_lt_mono; assumption. Qed.
imports: List Rbase Rfunctions