∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ℕ)
  (a : R), bi * i b = 1 → ∀ (f : Polynomial R), f.natDegree ≤ N → DenomsClearable a b N f i