proposition: Lemma unit_no_zero_divisor (x : R) {unit : RingUnit x}: ¬ZeroDivisor x.
proof: Proof. destruct unit as [y x_y_unit]. intros [_ [z [z_nonzero xz_zero]]]. destruct z_nonzero. transitivity ((x * z) * y); try (rewrite xz_zero; ring). transitivity (x * y * z); try (rewrite x_y_unit; ring). ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra