-1 *L m = -m. Proof. apply grp_moveL_1V. lhs nrapply (ap (_ +) (lm_unit m)^). lhs_V nrapply lm_dist_r. rhs_V nrapply lm_zero_l. f_ap. apply grp_inv_l. 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.