Merge pull request #2043 from Alizter/ps/rr/fix__proof_of_equiv_leq_l…

…t_or_eq Fix: proof of equiv_leq_lt_or_eq
HoTT · Aug 4, 2024 · f367ba9 · f367ba9
2 parents 59e94fd + 8a0d5a4
commit f367ba9
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v
@@ -854,8 +854,9 @@ Defined.
 Definition equiv_leq_lt_or_eq {n m} : (n <= m) <~> (n < m) + (n = m).
 Proof.
   srapply equiv_iff_hprop.
-  - rapply ishprop_sum.
-    intros H1 H2.
+  - nrapply ishprop_sum.
+    1,2: exact _.
+    intros H1 p; destruct p.
     contradiction (lt_irrefl _ _).
   - intro l; induction l.
     + now right.