proposition: Lemma nth_copy_in : forall n el x, x < n -> nth_error (copy n el) x = Some el.
proof: Proof. intros sn el x x_n. destruct (nth_error_In (copy sn el) x) as [[es es_nth] | en]. rewrite es_nth, (copy_in sn el es); trivial. eapply nth_some_in; eauto. assert (x >= length (copy sn el)). apply nth_beyond_idx; trivial. rewrite copy_length in H. absurd (x < sn); auto with arith. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)