proposition: Lemma nth_rec2up_indep d1 d2 m1 m2 n : n <= m1 -> n <= m2 -> nth d1 (rec2up m1) n = nth d2 (rec2up m2) n.
proof: Proof. move=> h1 h2. rewrite !nth_rev; first last. - by rewrite size_rec2down /=; move: h1 h2; iomega_le. - by rewrite size_rec2down /=; move: h1 h2; iomega_le. rewrite !size_rec2down /= !subSS. exact: nth_rec2down_indep. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp