proposition: Lemma shiftrepeat_nth A: forall n k (v: t A (S n)), nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
proof: Proof. intros n k. apply (fun P P0 PS => Fin.rectS P P0 PS k); clear n k. - intros [|n] v; rewrite (eta v); [|reflexivity]. now rewrite (nil_spec (tl v)). - intros n k IH v. rewrite (eta v). apply IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec