Fix build on Coq v8.12

coq-community · Sep 16, 2023 · 24fee67 · 24fee67
1 parent 12dd48f
commit 24fee67
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 12 deletions.
diff --git a/theories/ZornsLemma/FiniteTypes.v b/theories/ZornsLemma/FiniteTypes.v
@@ -1,4 +1,5 @@
 From Coq Require Import
+  Arith
   Description
   FunctionalExtensionality
   Lia.

diff --git a/theories/ZornsLemma/Finite_sets.v b/theories/ZornsLemma/Finite_sets.v
@@ -289,16 +289,12 @@ Proof.
   }
   replace (fun _ => _) with (Add (fun m => m < n) n).
   { constructor; auto.
-    intros ?. red in H.
-    apply Nat.lt_irrefl in H.
-    auto.
+    intros ?. red in H. lia.
   }
   clear IHn.
   apply Extensionality_Ensembles; split; intros m Hm.
   - inversion Hm; subst; clear Hm.
-    + cbv in *.
-      apply Nat.le_le_succ_r.
-      assumption.
+    + cbv in *. lia.
     + inversion H; subst; clear H.
       constructor.
   - cbv in *.
@@ -337,7 +333,7 @@ Proof.
   - apply (finite_nat_initial_segment_ens n).
   - auto.
   - intros ? ? ? ?.
-    destruct (Nat.eq_dec x y); [left|right]; auto.
+    destruct (PeanoNat.Nat.eq_dec x y); [left|right]; auto.
   - now intros m Hm; red; auto.
 Qed.
 

diff --git a/theories/ZornsLemma/ReverseMath/ReverseCSB.v b/theories/ZornsLemma/ReverseMath/ReverseCSB.v
@@ -3,10 +3,17 @@
    Also noteworthy: https://mathoverflow.net/questions/225819/how-strong-is-cantor-bernstein-schr%C3%B6der
 *)
 
-From ZornsLemma Require Import FiniteTypes FunctionProperties.
-From Coq Require Import FunctionalExtensionality ProofIrrelevanceFacts.
-From Coq Require Import PeanoNat ProofIrrelevance.
-From Coq Require Import RelationClasses.
+From ZornsLemma Require Import
+  FiniteTypes
+  FunctionProperties.
+From Coq Require Import
+  FunctionalExtensionality
+  Lia
+  PeanoNat
+  ProofIrrelevance
+  ProofIrrelevanceFacts.
+From Coq Require Import
+  RelationClasses.
 
 (* Definition 6 of the above paper *)
 Definition OmniscientT (O : Type) : Prop :=
@@ -109,7 +116,8 @@ Proof.
   simpl in *. red in H0, H1.
   rewrite Nat.ltb_irrefl in *.
   symmetry in H0.
-  apply Nat.ltb_ge in H0, H1.
+  apply Nat.ltb_ge in H0.
+  apply Nat.ltb_ge in H1.
   apply Nat.le_antisymm; assumption.
 Qed.