proposition: Lemma sternD_1n_H1 q n i: i <= 2^q -> nth 0 (sternD 1 n q.+1) i = nth 0 (stern11 q) i + n * nth 0 (stern01 q) i.
proof: Proof. move => h. have h': i <= 2 ^ q.+1 by rewrite expn2S - addnn (leq_trans h) //leq_addr. by rewrite sternD_1n_kl // stern_prop // nth_stern11_sym. 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)