proposition: Lemma idealrDE x y : (x + y) \in I = (x == - y %[mod quot]).
proof: Proof. by rewrite -idealrBE opprK. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)