From 2f906481423530b03f21ff605aaee3f281131608 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 31 Oct 2020 14:20:16 +0900
Subject: Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`

- Rename `eq_sorted` lemmas to `sorted_eq` to address a naming inconsistency.
- Lemma `sort_le_id` has been generalized from `orderType` to `porderType`.
---
 mathcomp/ssreflect/binomial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/binomial.v')

diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 836c323..cd3ec87 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -468,7 +468,7 @@ have ft_m: #|f_t t| = m.
   rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj).
   exact: (sorted_uniq ltn_trans ltnn).
 rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=.
-apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y.
+apply/eqP/(irr_sorted_eq ltn_trans ltnn) => // y.
 by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *.
 Qed.
 
-- 
cgit v1.2.3