proposition: Lemma mul_sum_omega a n: a != zero -> (T1omega * a + \F n) * T1omega = (T1omega * a) * T1omega.
proof: Proof. case: n; [ by rewrite T1addn0 | move => n]. elim: a => // a _ m b Hb _. rewrite T1mul_omega; case pa: (a== zero) => //. rewrite /T1nat {1}/T1add -/T1add T1ltn0 T1lt0n T1add_eq0 andFb /negb. rewrite {2 4} /T1omega /phi0 /T1mul -/T1mul andbF //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)