proposition: Lemma prime_idealrM u v : (u * v \in I) = (u \in I) || (v \in I).
proof: Proof. apply/idP/idP; last by case/orP => /idealMr hI; rewrite // mulrC. exact: prime_idealr_closed_subproof. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)