for R being non almost_left_invertible factorial domRing
for a being non zero NonUnit of R ex b being Element of R st b is_a_irreducible_factor_of a