proposition: Lemma nth_repeat : forall A n (x:A) k d, nth n (List.repeat x k) d = if le_lt_dec k n then d else x.
proof: Proof. intros. destruct (le_lt_dec k n). - apply nth_overflow. rewrite repeat_length. exact l. - apply (repeat_spec k x). apply nth_In. rewrite repeat_length. exact l. Qed.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos