proposition: Lemma nf_pred a: T2nf a -> T2nf (T2pred a).
proof: Proof. elim:a => // a _ b _ n c Hc /= /and4P [pa pb /Hc pc pe]. case pf: ([a, b] == one); first by apply: nf_finite. by rewrite /= pa pb pc (T2le_lt_trans (pred_le c) pe). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)