qed.
coercion cic:/matita/groups/eq_opp_plusr.con nocomposites.
lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y).
qed.
coercion cic:/matita/groups/eq_opp_plusr.con nocomposites.
lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y).