proposition: Lemma nf_pred a: T1nf a -> T1nf (T1pred a).
proof: Proof. elim:a => // a _ n b Hb /and3P [pa /Hb pb pc] /=. case az: (a== zero) => //; first by apply: nf_finite. by rewrite /= (T1le_lt_trans (pred_le b) pc) pb !andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)