fact: Fixpoint T3succ x := if x is cons a b c n d then if all_zero a b c then \F n.+2 else cons a b c n (T3succ d) else one.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)