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