Definition eqrelsubmodule : eqrel M. Proof. use eqrelconstr. - exact (λ m m', A (m - m')). - intros x y z xy yz. assert (K := submoduleadd A (x - y) (y - z) xy yz). rewrite (assocax M) in K. rewrite <- (assocax M (grinv _ y) y) in K. rewrite grlinvax in K. rewrite lunax in K. exact K. - intros x. rewrite (grrinvax M x). exact (submodule0 A). - intros x y axy. assert (K := submoduleinv A (x - y) axy). rewrite grinvop in K. rewrite grinvinv in K. exact K. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Modules.Core. Require Import UniMath.Algebra.Modules.Submodule.