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