proposition: Theorem head_loop1 (n p : nat) a s : head d s = a -> head d (loop1 n p a s) = iteri n (fun i c => F c (i + p)) a.
proof: Proof. elim: n p a s =>[//|n IHn] p a s H. move E: (n.+1) => n'. rewrite /= -{}E IHn //. clear; elim: n =>[//=|n IHn]. by rewrite /= IHn /= addSnnS. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp