proposition: Lemma expO_mul1 a b: (exp_O a b) * (one) = exp_O a b.
proof: Proof. rewrite /exp_O; case: eqP; [by move => ->; case: eqP | case: eqP => //]. case:(T1finite a) => //=; rewrite andbT; case: eqP => // -> //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)