Theorem not_irreducible_of_not_unit_dvdNotUnit

Modification history