proposition: Lemma map_nth_error_None_iff : 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 A B l f n ; revert l ; induction n ; intro l. destruct l ; simpl ; split ; auto ; intro H ; inversion H. destruct l ; simpl ; [split ; auto ; intro H ; inversion H | apply IHn]. 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