proposition: Lemma nf_succ a: T3nf a -> T3nf (T3succ a).
proof: Proof. elim:a => // a _ b _ c _ n d Hd /= /and5P [pa pb pc /Hd pd pe]. case az: (all_zero a b c) => //=; rewrite pa pb pc pd /=. by apply:limit_pr => //=; rewrite az. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)