proposition: Lemma nth_stern11 n i: i <= 2^n -> nth 0 (stern11 n) i = stern (2^n + i).
proof: Proof. move => h. by rewrite - split_stern01_right nth_drop stern_prop // expn2S -addnn leq_add2l. 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)