fact: Fixpoint loop1 (n p : nat) (a : T) (s : seq T) {struct n} : seq T := match n with | 0 => s | m.+1 => let c := F a p in loop1 m p.+1 c (c :: s) end.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp