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