proposition: Lemma grec1downE (n : nat) : grec1down n = if n >= size init then gloop1 (n - size init).+1 (size init) a0 (rev init) else rev (take n.+1 init).
proof: Proof. rewrite /grec1down. case: (leqP (size init) n)=>H; first by rewrite subSn //. by move: H; rewrite -subn_eq0; move/eqP->. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp