proposition: Lemma nf_exp a b: T1nf a -> T1nf b -> T1nf (a ^b).
proof: Proof. move => na nb. move: (nf_split nb) (proj1 (nf_rev nb)) => sa sb. rewrite /T1exp nf_mul // ?nf_expF // nf_expO //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)