proposition: Lemma apart_0_proper {x y} : x ≶ 0 → x = y → y ≶ 0.
proof: Proof. intros ? E. now rewrite <-E. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.strong_setoids MathClasses.theory.rings