proposition: Lemma fusc_middle_div k q (n := 2^k * (q.*2.+1)): fusc (n.-1) + (fusc n.+1) = (k.*2.+1) * fusc n.
proof: Proof. rewrite /n {n}; elim: k. by rewrite expn0 mul1n /= - doubleS fusc_odd !fusc_even // mul1n. move => n. rewrite expnS - mulnA mul2n /= fusc_even fusc_odd. rewrite fusc_podd ? muln_eq0 ?expn_eq0 //; set t:= _*_. rewrite (addnC (fusc t)) addnACA => ->. by rewrite addnn - (mul2n (fusc t)) -mulnDl addn2 mulSn. 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)