proposition: Lemma nf_succ a: T1nf a -> T1nf (T1succ a).
proof: Proof. elim:a => // a _ n b Hb /and3P [pa /Hb pb pc] /=. case az: (a== zero) => //; apply /and3P;split => //. by apply:limit_pr => //=; rewrite az. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)