Definition module_eqrelsubmodule : module_eqrel M. Proof. use make_module_eqrel. - exact eqrelsubmodule. - split. + intros a b c. assert (H : a - b = c + a - (c + b)). { etrans; [|eapply (maponpaths (λ z, z - (c + b))); apply (commax M)]; rewrite assocax. apply maponpaths. now rewrite grinvop, commax, assocax, grlinvax, runax. } simpl in *. now rewrite H. + intros a b c. assert (H : a - b = a + c - (b + c)). { rewrite assocax. apply maponpaths. now rewrite grinvop, <- (assocax M), grrinvax, lunax. } simpl in *. now rewrite H. - intros r m m'. assert (H : (r * m) - (r * m') = r * (m - m')) by now rewrite module_inv_mult, module_mult_is_ldistr. generalize (submodulemult A r (m - m')). simpl in *. now rewrite H. 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.