proposition: Lemma equiv_is_equiv : equiv_class_of equiv.
proof: Proof. split=> [x|x y|y x z]; rewrite !equivE ?subrr ?rpred0 //. by rewrite -opprB rpredN. by move=> *; rewrite -[x](addrNK y) -addrA rpredD. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)