proposition: Lemma sum_Stern1 n: \sum_(i<2^n) (Stern (i+2^n).*2) = (2^n)%N%:Q / 2%:Q.
proof: Proof. case: n; first by rewrite expn0 big_ord_recr /= big_ord0. move => n. set p := (2^n)%N. rewrite - (big_mkord xpredT (fun i => Stern (i + 2 ^ n.+1).*2)). transitivity (p%:Q); last by rewrite expnS ratN_M mulrC mulKf //. have ha: (0 <= 2^n)%N by []. have hb: (2^n <= 2^n.+1)%N by rewrite leq_exp2l. rewrite(big_cat_nat _ _ _ ha hb) /= [X in _ + X] big_nat_rev /=. rewrite -/p -{2} (add0n p) big_addn expn2S -{2} addnn addnK -big_split /=. rewrite big_mkord; transitivity (\sum_(i < p) 1 %:Q); last by rewrite sumr_const card_ord //. rewrite -/p; apply: eq_bigr => i _. have hc: (i + p < p.*2)%N by rewrite - addnn ltn_add2r (ltn_ord i). set a := (i + p.*2)%N. set c := (p + p.*2 - (i + p).+1 + p.*2)%N. have he1: (a + c.+1 = 3 * (2^n.+1))%N. rewrite /a/c - (addnBA _ hc) - addSn (addnC i) - addnA - addSn (addnA i). by rewrite (addnA i) addnS (subnKC hc) /p -expn2S addnn - mul2n -mulSn. have he2: (a.+1 + c = 3 * (2^n.+1))%N. by rewrite addSnnS he1. have lt0: (a < (2^n.+1).*2)%N. rewrite expn2S -/p /a -(addnn p.*2) ltn_add2r - addnn ltn_addr //. have hl1: ((2^n.+1) <= a <= (2^n.+1).*2)%N. by rewrite (ltnW lt0) expn2S -/p /a leq_addl //. have hl2: ((2^n.+1) <= a.+1 <= (2^n.+1).*2)%N. rewrite lt0 expn2S -/p /a ltnW // ltnS leq_addl //. rewrite /Stern ! fusc_even ! fusc_odd. rewrite - (fusc_palindrome hl1 he1) - (fusc_palindrome hl2 he2) addnC. by rewrite - mulrDl addrC -ratN_D divff // addnC - fusc_odd fuscq_eq0. 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)