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