{R : Ring} {M N : LeftModule R} : LeftModuleIsomorphism M N -> LeftModuleIsomorphism N M. Proof. intros f. snrapply Build_LeftModuleIsomorphism. - snrapply Build_LeftModuleHomomorphism'. + exact f^-1. + intros r m n. apply moveR_equiv_V. rhs nrapply grp_homo_op. symmetry. f_ap. 2: apply eisretr. lhs nrapply lm_homo_lact. apply ap. apply eisretr. - exact _. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.