proposition: Lemma gloop1S_ex n p a s : exists c, gloop1 n.+1 p a s = c :: (gloop1 n p a s).
proof: Proof. elim: n p a s => [|n IH] p a s; first by exists (G a p). remember (S n) as n'; simpl. case: (IH p.+1 (F a p.+1) (G a p :: s))=> [c Hc]. rewrite Hc {}Heqn' /=. by exists c. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp