Theorem WfDvdMonoid.not_unit_iff_exists_factors_eq

Modification history