proposition: Lemma rec1down_co0 n: nth d (rec1down n) n = a0.
proof: Proof. elim: n=> [//|n IH]. by rewrite /rec1down; have [c ->] := loop1S_ex n 1 a0 [:: a0]. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp