proposition: Lemma map_nth_error_None : forall {A B : Type} (l : list A) (f : A -> B) (n : nat), nth_error l n = None -> nth_error (map f l) n = None.
proof: Proof. intros ; apply map_nth_error_None_iff ; assumption. 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