proposition: Lemma sternD_1n_member a n: (exists k i, i <=2^k /\ a = nth 0 (sternD 1 n k) i) <-> (a==1 \/ n <= a).
proof: Proof. split. move => [k [i [pa ->]]]; rewrite sternD_1n_kl // !sternD_fusc. case iz: (i==0); first by left; rewrite (eqP iz) subn0 fusc_pow2 muln0 addn0. have h: n <= n * fusc i by rewrite leq_pmulr // fusc_gt0 lt0n iz. by right; rewrite (leq_trans h) // leq_addl. case => ap; first by rewrite (eqP ap);exists 0, 0. have ha: 0 < 2 ^ (a - n) by rewrite expn_gt0. exists (a-n), 1; split => //; rewrite sternD_1n_kl // muln1 subn1. by rewrite sternD_fusc fusc_pred_pow2 subnK. 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)