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