proposition: Lemma Stern_pred_pow2 n: Stern ((2^n).-1) = n%:Q.
proof: Proof. move: (expn_gt0 2 n) => /= /prednK eq. by rewrite /Stern eq fusc_pow2 fusc_pred_pow2 divr1. 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)