proposition: Lemma expO_add z u v: exp_O z u * exp_O z v = exp_O z (u + v).
proof: Proof. rewrite /exp_O; case: eqP. move ->; case: eqP; first by move ->;rewrite T1mul1n //. by move /eqP => uz;rewrite T1add_eq0 (negbTE uz) T1mul0n. by case: eqP => //_ _;case (T1finite z); rewrite - mul_phi0 // mul_distr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)