proposition: Lemma fusc_col_progression i j: j <= 2 ^ i -> fusc(2^ (i.+1) + j) = fusc(2 ^ i + j) + fusc j.
proof: Proof. elim: i j; [by case => // [] [] | move => n Hrec j]. rewrite expn2S expn2S - (odd_double_half j); case: (odd j). rewrite ltn_double ! addnS - !doubleD !fusc_odd addnACA => sa. by rewrite (Hrec _ (ltnW sa)) - addnS - addnS Hrec. by rewrite leq_double - !doubleD ! fusc_even; apply: Hrec. 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)