proposition: Lemma RList_P12 : forall (l:list R) (i:nat) (f:R -> R), (i < length l)%nat -> pos_Rl (map f l) i = f (pos_Rl l i).
proof: Proof. simple induction l; [ intros; elim (Nat.nlt_0_r _ H) | intros; induction i as [| i Hreci]; [ reflexivity | simpl; apply H; apply Nat.succ_lt_mono; apply H0 ] ]. Qed.
imports: List Rbase Rfunctions