From b99023e783e5d14941574420356dfa62e51f75fe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 Mar 2017 14:26:24 +0100
Subject: [PATCH] Derive monoid_right_id.

---
 theories/algebra/monoid.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/monoid.v b/theories/algebra/monoid.v
index f933e57d0..bf6d1f14e 100644
--- a/theories/algebra/monoid.v
+++ b/theories/algebra/monoid.v
@@ -23,10 +23,11 @@ Class Monoid {M : ofeT} (o : M → M → M) := {
   monoid_assoc : Assoc (≡) o;
   monoid_comm : Comm (≡) o;
   monoid_left_id : LeftId (≡) monoid_unit o;
-  monoid_right_id : RightId (≡) monoid_unit o;
 }.
 Lemma monoid_proper `{Monoid M o} : Proper ((≡) ==> (≡) ==> (≡)) o.
 Proof. apply ne_proper_2, monoid_ne. Qed.
+Lemma monoid_right_id `{Monoid M o} : RightId (≡) monoid_unit o.
+Proof. intros x. etrans; [apply monoid_comm|apply monoid_left_id]. Qed.
 
 (** The [Homomorphism] classes give rise to generic lemmas about big operators
 commuting with each other. *)
-- 
GitLab