proposition: Lemma nth_rec1down_indep d1 d2 m1 m2 n : n <= m1 -> n <= m2 -> nth d1 (rec1down m1) (m1 - n) = nth d2 (rec1down m2) (m2 - n).
proof: Proof. move=> h1 h2. have h1' := subnKC h1; have h2' := subnKC h2. case: (ltngtP m1 m2)=> Hm; last first. - by rewrite Hm (nth_defaults d1 d2) // size_rec1down; iomega. - set p := m2 - n in h2' *. rewrite -h2' addnC. pose q := m1 - m2. have Hpq : m1 - n = p + q. rewrite /p /q in h2' *. by rewrite addnC addnBA // subnK // ltnW. rewrite Hpq. have->: m1 = p + q + n by rewrite -Hpq subnK. exact: nth_rec1downD_dflt2. set p := m1 - n in h1' *. rewrite -h1' addnC. pose q := m2 - m1. have Hpq : m2 - n = p + q. rewrite /p /q in h2' *. by rewrite addnC addnBA // subnK // ltnW. rewrite Hpq. have->: m2 = p + q + n by rewrite -Hpq subnK. symmetry; exact: nth_rec1downD_dflt2. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp