proposition: Lemma split_limit x: ((T2split x).2 == 0) = ((x==zero) || T2limit x).
proof: Proof. elim: x => // a _ b _ n c Hc /=. case: ([a, b] == one) => //; rewrite - Hc; by case: (T2split c). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)