proposition: Lemma size_rec2down n : size (rec2down n) = n.+1.
proof: Proof. by case: n => [//|[//|n]]; rewrite size_loop2 addn2. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp