proposition: Lemma nth_rec1downD d1 p q n : nth d1 (rec1down (p+q+n)) (p+q) = nth d1 (rec1down (p+n)) p.
proof: Proof. elim: q=> [|q IH]; first by rewrite addn0. by rewrite !addnS addSn -nth_behead behead_rec1down. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp