proposition: Lemma fusciL_valn n: FusciL (list_of_num (bin_of_nat n)) 1 0 = fusc n.
proof: Proof. case: n => // n. move:(nat_list_succ' n); set q := list_of_num (bin_of_nat n.+1) => /eqP eq. by rewrite eq fusciL_val nat_of_list_rT - eq /q list_of_numK bin_of_natK. 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)