proposition: Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.
proof: Proof. move=> x y /=; unlock add; apply/eqP; rewrite piE equivE. rewrite opprD addrAC addrA -addrA. by rewrite rpredD // (idealrBE, idealrDE) ?pi_opp ?reprK. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)