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