proposition: Lemma split_succ x: let:(y,n):= T1split x in T1split (T1succ x) = (y,n.+1).
proof: Proof. elim: x => // a _ n b /=. by case pa: (a==zero) => //=; rewrite pa /=; case: (T1split b) => u v ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)