fact: Fixpoint nn_to_n_split l: (seq bool * seq bool) := if l is a::l1 then if l1 is b::l2 then let r := nn_to_n_split l2 in (a:: r.1, b:: r.2) else ([::a], [::false]) else (nil,nil).
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)