fact: Fixpoint pos_of_list l := match l with | [ :: _ ] => xH | a :: l => if a then xI (pos_of_list l) else xO (pos_of_list l) | nil => xH 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)