proposition: Lemma map_nth_error2 {A B : Type} : forall f l p, nth_error l p = @None A -> nth_error (map f l) p = @None B.
proof: Proof. intros f l p ; revert l ; induction p ; intro l ; destruct l. trivial. intro Hf ; inversion Hf. trivial. simpl ; apply IHp. Qed.
imports: Rsequence_def Rsequence_sums_facts Rpser Rfunction_facts Rextensionality Rfunction_classes Nth_derivative_def Nth_derivative_facts Dequa_def List PeanoNat Tactics Option