fact: Definition stack_of_bitseq : bitseq -> bit_stack := foldr (fun b => if b then Bpush1 else Bpush0) Bstack0.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype) fourcolor(color)