proposition: Lemma pow_omega x: T1nf x -> T1omega ^x = phi0 x.
proof: Proof. move => nx; rewrite {2} (proj2 (nf_rev nx)) /T1exp mul_phi0;congr T1mul. by elim (T1split x).2 => // n /= -> ;rewrite /T1omega - mul_phi0; case n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)