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