proposition: Lemma split_is_succ x: ((T2split x).2 != 0) = (T2is_succ 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)