proposition: Lemma sternD_nth_odd u v n k: k < 2^n -> nth 0 (sternD u v n.+1) (k.*2.+1) = nth 0 (sternD u v n) k + nth 0 (sternD u v n) k.+1.
proof: Proof. rewrite {1} /sternD -/(sternD ) - ltnS -(size_sternD u v n). move: {u v n} (sternD u v n); elim:k; first by case => // a; case. move => n Hrec [] // a [] // b l; rewrite ltnS => ww;apply: (Hrec (b:: l) ww). 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)