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