proposition: Lemma div_by_omega_pr x: T1nf x -> ((x==zero) || T1limit x) -> T1omega * (T1div_by_omega x) = x.
proof: Proof. elim: x => // a _ n b Hb. rewrite orFb /T1limit -/T1limit; case pa: (a==zero) => //. move: (negbT pa); rewrite - T1ge1; case /orP. move /eqP => <-. rewrite /T1div_by_omega -/T1div_by_omega T1subnn T1mul_omega eqxx. case b => // a' n' b' /=; move /andP => [_]. by rewrite T1lt1 T1ltn0 ! if_same if_simpl => ->. move => lt1 /and3P [na /Hb h _] /h h'. rewrite /T1div_by_omega -/T1div_by_omega T1mul_omega h'. by rewrite - (sub1a (negbT pa) na) (negbTE (sub_nz na lt1)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)