proposition: Lemma nf_expO a b: T1nf a -> T1nf b -> T1nf (exp_O a b).
proof: Proof. move => na nb; rewrite /exp_O; case: eqP => //; case: eqP => //. by rewrite fun_if !nf_phi0 nf_mul ? nb // ?nf_mul // ? nf_log // if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)