proposition: Lemma nf_div_by_omega x: T1limit x -> T1nf x -> T1nf (T1div_by_omega x).
proof: Proof. elim: x => // a _ n b Hb /= lx /and3P [sa sb sc]; apply /and3P; split => //. + by apply: nf_sub. + move: lx; case eqP => //_;case /orP; first by move /eqP -> . by move => lb ; apply: Hb. move: lx; case pa: (a==zero) => // h. have oz: T1omega != zero by done. have nz: T1nf (phi0 (a - cons zero 0 zero)) by rewrite nf_phi0 nf_sub //. rewrite - (T1lt_mul2l (T1div_by_omega b) oz nz) div_by_omega_pr //. by rewrite -[T1omega ]/(phi0 (one)) - mul_phi0 - sub1a // pa. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)