proposition: Lemma split_finite x: ((T3split x).1 == zero) = T3finite x.
proof: Proof. case x => // a b c n d //=. by case pa: (all_zero a b c) => //;case: T3split x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)