proposition: Lemma head_loop1S n s a p : head d s = a -> head d (loop1 n.+1 p a s) = F (head d (loop1 n p a s)) (n+p).
proof: Proof. by elim: n s a p => [_ _ _->//|n IHn s a p H]; rewrite !IHn // addSnnS. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp