proposition: Lemma fusc_is_even1 n: fusc n + fusc n.+2 = fusc (n.+1) %[mod 2].
proof: Proof. case: (elogn2P n) => k q eq. move:(fusc_middle_div k q) => /=; rewrite -eq succnK => ->. by rewrite - modnMm -add1n -modnDm /= -muln2 modnMl addn0 // mul1n modn_mod. 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)