proposition: Lemma factor_ring_eq_0 (x y : Factor A P) : x = 0 ↔ P ('x).
proof: Proof. transitivity (P ('x - cast (Factor A P) A 0)). intuition. apply ideal_proper. unfold cast. simpl. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.ring_congruence