proposition: Lemma factor_ring_eq (x y : Factor A P) : x = y ↔ P ('x - 'y).
proof: Proof. intuition. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.ring_congruence