Removed not_symmetry from stdpp_tactics.v, importing not_symmetry fro…

…m MathClasses.misc.util
coq-community · Jul 30, 2024 · b4d9a0e · b4d9a0e
1 parent 99feb0c
commit b4d9a0e
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/stdpp/stdpp_tactics.v b/stdpp/stdpp_tactics.v
@@ -1,8 +1,7 @@
+Require Import
+  MathClasses.misc.util.
 From Coq Require Export RelationClasses Relation_Definitions Lia.
 
-Lemma not_symmetry {A} `{R : relation A, !Symmetric R} x y : ~ R x y -> ~ R y x.
-Proof. intuition. Qed.
-
 Ltac fast_done :=
   solve
     [ eassumption