proposition: Theorem nth_grec1up_indep (d1 d2 : T) (m1 m2 n : nat) : n <= m1 -> n <= m2 -> nth d1 (grec1up m1) n = nth d2 (grec1up m2) n.
proof: Proof. move=> h1 h2; rewrite !nth_rev; try by rewrite size_grec1down. rewrite !size_grec1down !subSS; exact: nth_grec1down_indep. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp