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