proposition: Lemma succ_pred x: T1nf x -> T1is_succ x -> x = T1succ (T1pred x).
proof: Proof. elim: x => // a _ n b Hb; case az: (a==zero). by rewrite (eqP az) T1nf_finite1 => /eqP ->; case: n. by move => /T1nf_consb /Hb h /=;rewrite /= az /= az => h'; rewrite - h. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)