proposition: Lemma Stern_palindrome a: (0 < a)%N -> (Stern a)^-1 = Stern ((3* 2^(log2 a).-1 -a).-1).
proof: Proof. case: a => // a _. move: (log2_bnd a) => /andP[]; rewrite {2}log2S_k. set n := (log2 a.+1).-1; set b := _.-1; move => sa sb. have eb: b = ((2 ^ n.+1 - a.+2) + 2^n)%N. by rewrite /b -subnS mulSn - expnS - addnBA // addnC. rewrite expn2S in sb. have sc: (2^n <= b)%N by rewrite eb; apply: leq_addl. have sd: (b < (2^n).*2)%N by rewrite eb expn2S -{2}(subnK sb) ltn_add2l ltnS. have Ha: (2 ^ n <= a.+2 <= (2 ^ n).*2)%N by rewrite (leqW sa) sb. have Hc: (2 ^ n <= a.+1 <= (2 ^ n).*2)%N by rewrite sa (ltnW sb). have eab:(a.+2 + b = 3 * 2 ^ n)%N. by rewrite eb addnA expn2S (subnKC sb) -muln2 -mulnSr mulnC. rewrite /Stern (fusc_palindrome Ha eab). by rewrite addSnnS in eab; rewrite(fusc_palindrome Hc eab) invf_div. 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)