proposition: Lemma sum_Stern_simp n: \sum_(2^n<=i< 2^n.+1) 1/((fusc i) * (fusc i.+1))%N%:Q = 1%:Q.
proof: Proof. rewrite expn2S -addnn. pose f k := \sum_(2 ^ n <= i < 2 ^ n + k) 1 / (fusc i * fusc i.+1)%N%:Q. suff: forall i, (i <= 2^n)%N -> f i = (fusc i)%:Q / (fusc (2^n +i)%N) %:Q. by move => H; rewrite -/(f _) H // addnn - expn2S ! fusc_pow2. move => i;rewrite/f - {2} (add0n (2 ^ n)%N) big_addn addKn big_mkord. elim:i; first by rewrite big_ord0 mul0r. move => i Hrec lim. have hu: (fusc (2 ^ n + i))%:Q != 0. by rewrite fuscq_eq0 addn_eq0 expn_eq0. have hv:(fusc (2 ^ n + i.+1))%:Q != 0. by rewrite addnS fuscq_eq0. rewrite big_ord_recr /= (Hrec (ltnW lim)) -addSn (addnC i) (addnC i.+1). rewrite div1r ratN_M invrM ?unitfE // - mulrDl addf_inv // -ratN_M mulnC. rewrite -{2}[1]/(1%N%:Q) - ratN_D addnC -(fusc_bezout2 lim). by rewrite mulrAC mulnC ratN_M mulfK. 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)