proposition: Lemma T1finite_succ x: T1finite x -> T1finite (T1succ x).
proof: Proof. elim: x => // a Ha n b Hb; move /eqP => -> //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)