proposition: Lemma sum_Stern n: \sum_(i<2^n) (Stern (i+2^n)) = ((3* 2^n)%N%:Q -1) / 2%:Q.
proof: Proof. elim:n. rewrite expn0 big_ord_recr /= big_ord0 add0r add0n /Stern /fusc /=. by apply/val_inj. move => n Hrec. set p := (2^n)%N%:Q. pose f i := Stern (i + (2 ^ n).*2). have Hu m: \sum_(i < m.*2) f i = \sum_(i < m) f i.*2 + \sum_(i < m) f i.*2.+1. elim:m; first by rewrite !big_ord0. by move => m Hr; rewrite doubleS !big_ord_recr /= Hr addrACA addrA. have Ha: \sum_(i < 2 ^ n) f i.*2 = p / 2%:Q. by rewrite - sum_Stern1; apply: eq_bigr => i _; rewrite doubleD. have Hb: p = p * 2%N%:Q / 2%N%:Q by rewrite mulfK. have Hc: p = \sum_(i < 2 ^ n) 1 by rewrite sumr_const card_ord. have Hd: \sum_(i<2^n) f i.*2.+1 = p + (3%N%:Q * p -1)/2%N%:Q. rewrite /f -ratN_M - Hrec Hc - big_split /=; apply eq_bigr => i _. rewrite addSn -doubleD /Stern -doubleS fusc_even fusc_odd ratN_D addf_div1 //. by rewrite fuscq_eq0. rewrite expn2S Hu Hd Ha {2}Hb -mulrDl -mulrDl addrA addrA - ratN_M - ratN_M. by rewrite - ratN_D - ratN_D -mulnS mulnC addnn doubleMr. 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)