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