proposition: Lemma nth_after_copy : forall n el el', nth_error (copy n el' ++ el::nil) n = Some el.
proof: Proof. intros. rewrite nth_app_right, copy_length. replace (n - n) with 0; [trivial | lia]. rewrite copy_length. auto with arith. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)