proposition: Lemma behead_loop2 n s a b p : behead (loop2 n.+1 p a b s) = loop2 n p a b s.
proof: Proof. by elim: n s a b p => [//|n IHn] s a b p; rewrite IHn. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp