proposition: Lemma head_loop2S n s a b p : hb d s = a -> head d s = b -> let s' := (loop2 n p a b s) in head d (loop2 n.+1 p a b s) = F (hb d s') (head d s') (n+p).
proof: Proof. elim: n s a b p => [|n IHn] s a b p Ha Hb; first by rewrite /= Ha Hb. by rewrite IHn // addSnnS. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp