proposition: Lemma split_is_succ x: ((T1split x).2 != 0) = (T1is_succ x).
proof: Proof. elim: x => // a _ n b Hb /=. case pa: (a==zero) => //; rewrite - Hb; by case: (T1split b). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)