proposition: Lemma size_grec1up n : size (grec1up n) = n.+1.
proof: Proof. by rewrite size_rev size_grec1down. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp