proposition: Lemma split_finite x: ((T2split x).1 == zero) = T2finite x.
proof: Proof. case x => // a b n c //=. by case pa: ([a, b] == one) => //;case: T2split x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)