From 94277d6df985261eb916213019ea13b70e63b2d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Oct 2020 19:18:23 +0200
Subject: [PATCH] exploit irreflexivity
---
theories/algebra/dfrac.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index adf77d0fa..4b2a013f6 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -127,7 +127,7 @@ Section dfrac.
intros [q| |q];
rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
- apply (Qp_not_plus_ge 1 q).
- - move=>/Qclt_not_eq. intros Heq. apply Heq. done.
+ - intros []%irreflexivity. apply _.
- move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
Qed.
--
GitLab