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