proposition: Lemma rquot_IdomainAxiom (x y : {quot I}): x * y = 0 -> (x == 0) || (y == 0).
proof: Proof. by move=> /eqP; rewrite -[x]reprK -[y]reprK !piE !equivE !subr0 prime_idealrM. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)