proposition: Theorem head_gloop1 (d : T) (n p : nat) (a : A) (s : seq T): head d (gloop1 n.+1 p a s) = G (iteri n (fun i c => F c (i + p).+1) a) (n + p).
proof: Proof. elim: n p a s =>[//|n IHn] p a s. move E: (n.+1) => n'. rewrite /= -{}E IHn. congr G; last by rewrite addSnnS. 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