fact: Fixpoint bin_invert_aux L := match L with | true :: L' => true :: [seq ~~ i | i <- L'] | false :: L' => false :: bin_invert_aux L' | nil => nil end.
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)