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