proposition: Lemma succ_p1 x: T2is_succ (T2succ x).
proof: Proof. by elim: x => // a _ b _ n c Hc /=; case:([a, b] == one) => //=;rewrite Hc orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)