proposition: Lemma nth_grec1downD_dflt2 d1 d2 p q n: nth d1 (grec1down (p+q+n)) (p+q) = nth d2 (grec1down (p+n)) p.
proof: Proof. rewrite nth_grec1downD (set_nth_default d1 d2) //. by rewrite size_grec1down ltnS leq_addr. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp