proposition: Lemma sum_fusc_row n: \sum_(2^n <= i < 2^n.+1) (fusc i) = 3 ^n.
proof: Proof. transitivity (\sum_(i < 2^n) (fusc (i + 2^n))). by rewrite -{1}(add0n (2^n)) big_addn expn2S - addnn addnK big_mkord. elim:n => //; first by rewrite expn0 big_ord_recr /= big_ord0. move => n Hrec. rewrite expn2S (split_sum_even_odd1 (fun i =>fusc (i + (2 ^ n).*2))). have ->: \sum_(i < 2 ^ n) fusc (i.*2 + (2 ^ n).*2) = 3^n. by rewrite - Hrec; apply: eq_bigr => i _; rewrite -doubleD fusc_even. rewrite expnS mulSn - {3}Hrec mul2n - [in RHS] addnn; congr addn. have {2} ->: \sum_(i < 2 ^ n) fusc (i + 2 ^ n) = \sum_(i < 2 ^ n) fusc (i.+1 + 2 ^ n). have ep: 0 < 2 ^n by rewrite expn_gt0. rewrite -(prednK ep) big_ord_recl big_ord_recr /= addnC (prednK ep). rewrite add0n addnn fusc_even //. rewrite - big_split /=; apply: eq_bigr => i _. by rewrite addSn - doubleD fusc_odd addSn. 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)