proposition: Lemma sternD_1n_v' n q i: i <= 2^q -> nth 0 (sternD 1 n.+1 q) i = stern (2^ (q + n) + i).
proof: Proof. move => h; rewrite sternD_1n_v // nth_stern11 //; apply: (leq_trans h). by rewrite expnD; apply: leq_pmulr; rewrite expn_gt0. 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)