proposition: Lemma sternD_1n_H2 q n i: i <= 2^ q -> nth 0 (sternD 1 n q.+1) (i + 2^q) = nth 0 (sternD 1 0 q) i + n * nth 0 (stern11 q) i.
proof: Proof. move => ha. have hb: i + 2 ^ q <= 2 ^ q.+1 by rewrite expn2S -addnn leq_add2r. rewrite sternD_1n_kl// expn2S -addnn nth_stern11 // (addnC i); congr addn. by rewrite sternD_1n_kl // mul0n addn0 subnDl. 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)