proposition: Lemma sternD_1n_v n q i: i <= 2^q -> nth 0 (sternD 1 n.+1 q) i = nth 0 (stern11 (q + n)) i.
proof: Proof. elim: n q i; first by move => k i h;rewrite addn0. move => n Hrec k i la. rewrite - (add1n n.+1) -split_sternD_left nth_take ? ltnS // - addSnnS Hrec //. by rewrite expn2S -addnn (leq_trans la) // leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)