proposition: Lemma nth_error_map : forall n l, nth_error (map l) n = option_map f (nth_error l n).
proof: Proof. intro n. induction n as [|n IHn]; intro l. - now destruct l. - destruct l as [|? l]; [reflexivity|exact (IHn l)]. Qed.
imports: PeanoNat