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