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