r *L -m = - (r *L m). Proof. apply grp_moveL_1V. lhs_V nrapply lm_dist_l. rhs_V nrapply lm_zero_r. 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.