proposition: Lemma succ_p1 x: T1is_succ (T1succ x).
proof: Proof. by elim: x => // a _ n b Hb /=; case pa: (a==zero) => //=; rewrite pa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)