proposition: Lemma size_gloop1 n p a s : size (gloop1 n p a s) = n + size s.
proof: Proof. by elim: n p a 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