proposition: Lemma nth_nth_nth_map A : forall (l : list A) n d ln dn, n < length ln \/ length l <= dn -> nth (nth n ln dn) l d = nth n (map (fun x => nth x l d) ln) d.
proof: Proof. intros l n d ln dn Hlen. rewrite <- (map_nth (fun m => nth m l d)). destruct Hlen. - apply nth_indep. now rewrite map_length. - now rewrite (nth_overflow l). Qed.
imports: PeanoNat