proposition: Lemma rec1up_co0 n : nth d (rec1up n) 0 = a0.
proof: Proof. by rewrite nth_rev size_rec1down // subn1 rec1down_co0. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp