`{Funext} {R : Ring} {M N : LeftModule R} (f : M $-> N) : M / lm_kernel f ≅ lm_image f. Proof. snrapply Build_LeftModuleIsomorphism'. 1: rapply abgroup_first_iso. intros r. srapply Quotient_ind_hprop; intros m. apply path_sigma_hprop; simpl. apply lm_homo_lact. 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.