proposition: Lemma sternD_1n_H2' q n i: i <= 2^ q -> nth 0 (sternD 1 n q.+1) (2^q.+1 - i) = nth 0 (stern01 q) i + n * nth 0 (stern11 q) i.
proof: Proof. move => ha. have hb: i <= 2 ^ q.+1 by rewrite expn2S- addnn (leq_trans ha) // leq_addr. rewrite sternD_rev nth_rev size_sternD ? ltnS ? leq_subr //. rewrite subnS subSKn subKn // sternD_stern // mul1n stern_prop //. by rewrite nth_stern11_sym ? leq_subr // expn2S -addnn addnC. 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)