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