proposition: Lemma split_is_succ x: ((T3split x).2 != 0) = (T3is_succ x).
proof: Proof. elim: x => // a _ b _ c _ n d Hd /=. case pa: (all_zero a b c) => //; rewrite - Hd; by case: (T3split d). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)