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