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