fact: Fixpoint T2split x:= if x is cons a b n c then if ([a,b]==one) then (zero, n.+1) else let: (x, y) := T2split c in (cons a b n x,y) else (zero,0).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)