proposition: Lemma size_grec1down n : size (grec1down n) = n.+1.
proof: Proof. rewrite /grec1down. case E: (n.+1 - size init) =>[|k]. rewrite size_rev size_take. move/eqP: E; rewrite subn_eq0 leq_eqVlt. case/orP; last by move->. move/eqP->; rewrite ifF //. by rewrite ltnn. rewrite size_gloop1 /= -E. by rewrite size_rev subnK // ltnW // -subn_gt0 E. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp