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