proposition: Lemma pi_opp : {morph \pi : x / - x >-> opp x}.
proof: Proof. move=> x; unlock opp; apply/eqP; rewrite piE equivE. by rewrite -opprD rpredN idealrDE opprK reprK. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)