proposition: Lemma plus_int_Ox n x: x != zero -> \F n + T1omega * x = T1omega * x.
proof: Proof. case: n => // n xnz. by move:(mul_omega_limit xnz); case (T1omega * x) => // a m b /=; case a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)