proposition: Lemma pi_mul: {morph \pi : x y / x * y >-> mul x y}.
proof: Proof. move=> x y; unlock mul; apply/eqP; rewrite piE equivE. rewrite -[_ * _](addrNK (x * repr (\pi_{quot idealI} y))) -mulrBr. rewrite -addrA -mulrBl rpredD //. by rewrite idealMr // idealrDE opprK reprK. by rewrite mulrC idealMr // idealrDE opprK reprK. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)