fact: Definition fusc n := let fix loop n k := if k is k'.+1 then if n<=1 then n else if (odd n) then (loop n./2 k') + loop (uphalf n) k' else loop n./2 k' else 0 in loop n n.
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)