From 7f355343ee30f72d8ab3ce87f897dc0092e43c29 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Sun, 31 May 2020 00:24:10 +0900
Subject: tentative changelog

- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`
---
 mathcomp/algebra/ssrnum.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 6dbfaf7..f7b2e0f 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -5619,6 +5619,7 @@ Ltac mexact x := by mapply x.
 Local Notation min := minr.
 Local Notation max := maxr.
 
+Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed.
 Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed.
 Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed.
 Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed.
-- 
cgit v1.2.3