proposition: Lemma nth_rec2downD_dflt2 d1 d2 p q n : nth d1 (rec2down (p+q+n)) (p+q) = nth d2 (rec2down (p+n)) p.
proof: Proof. rewrite nth_rec2downD (nth_defaults d1 d2) // size_rec2down. by iomega. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp