From 593ce92e2e747b9f4af5258149ffc5e5f865bca0 Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Sun, 11 Feb 2024 01:17:13 +0100
Subject: [PATCH] Used Order.NatMonotonyTheory.nondecn_inP

---
 Makefile                   | 26 ++++++++++++++++++--------
 theories/SymGroup/Bruhat.v | 10 +++++-----
 2 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/Makefile b/Makefile
index cce329f..e6a8ec7 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.18.0
+## GNUMakefile for Coq 8.19.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.18.0
+COQMAKEFILE_VERSION:=8.19.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -307,6 +307,14 @@ else
   TIMING_ARG=
 endif
 
+ifneq (,$(PROFILING))
+  PROFILE_ARG=-profile $<.prof.json
+  PROFILE_ZIP=gzip $<.prof.json
+else
+  PROFILE_ARG=
+  PROFILE_ZIP=true
+endif
+
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -808,12 +816,13 @@ ifneq (,$(filter grouped-target,$(.FEATURES)))
 define globvorule=
 
 # take care to $$ variables using $< etc
-  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
-	$(SHOW)COQC $(1).v
-	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v
+  $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
+	$$(SHOW)COQC $(1).v
+	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
+	$$(HIDE)$$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
-	$(SHOW)COQNATIVE $(1).vo
-	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
+	$$(SHOW)COQNATIVE $(1).vo
+	$$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo
 endif
 
 endef
@@ -821,7 +830,8 @@ else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
+	$(HIDE)$(PROFILE_ZIP)
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@
diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v
index 3cb1d68..4a29957 100644
--- a/theories/SymGroup/Bruhat.v
+++ b/theories/SymGroup/Bruhat.v
@@ -74,11 +74,11 @@ Lemma bounded_le_homo (m n : nat) f :
   (forall i, m <= i < n -> f i <= f i.+1) ->
   {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}.
 Proof.
-move=> H i j /[!inE] lein.
-elim: j => [_ /[!leqn0]/eqP -> // | j IHj].
-move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij].
-have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply.
-by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW.
+rewrite -!leEnat => H; apply Order.NatMonotonyTheory.nondecn_inP.
+  move=> i j /[!inE] /andP[lemi _] /andP[_ lejn].
+  move=> k /andP[/ltW/(le_trans lemi) lemk /ltW/le_trans/(_ lejn) lekn].
+  by rewrite inE lemk lekn.
+by move=> i /[!inE] /andP[lemi _] /andP[_ lein]; apply: H; rewrite lemi.
 Qed.
 
 Lemma telescope_sumn_in2 n m f : n <= m ->