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/ssreflect/order.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'mathcomp/ssreflect')

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index d8bcff1..59de10c 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -74,6 +74,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* For x, y of type T, where T is canonically a porderType d:                 *)
 (*            x <= y <-> x is less than or equal to y.                        *)
 (*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
+(*           min x y <-> if x < y then x else y                               *)
+(*           max x y <-> if x < y then y else x                               *)
 (*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
 (*             x > y <-> x is greater than y (:= y < x).                      *)
 (*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
-- 
cgit v1.2.3