proposition: Lemma modular_ring_eq (x y : Mod b) : x = y ↔ ∃ k, 'x = 'y + b * k.
proof: Proof. split; intros [k E]; exists k. rewrite <-E. ring. rewrite E. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.theory.integers MathClasses.theory.ring_ideals