From 9fbe44b69b0a794476101a785be5b5042adedf78 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 Jun 2019 12:28:07 +0200
Subject: [PATCH] Define `Involutive` in terms of `Cancel`.

---
 theories/base.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index be57c2fe..9a066b98 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -327,8 +327,11 @@ Class Trichotomy {A} (R : relation A) :=
   trichotomy x y : R x y ∨ x = y ∨ R y x.
 Class TrichotomyT {A} (R : relation A) :=
   trichotomyT x y : {R x y} + {x = y} + {R y x}.
-Class Involutive {A} (R : relation A) (f : A → A) :=
-  involutive x : R (f (f x)) x.
+
+Notation Involutive R f := (Cancel R f f).
+Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x :
+  R (f (f x)) x.
+Proof. auto. Qed.
 
 Arguments irreflexivity {_} _ {_} _ _ : assert.
 Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
@@ -346,7 +349,6 @@ Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
 Arguments total {_} _ {_} _ _ : assert.
 Arguments trichotomy {_} _ {_} _ _ : assert.
 Arguments trichotomyT {_} _ {_} _ _ : assert.
-Arguments involutive {_ _} _ {_} _ : assert.
 
 Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
 Proof. intuition. Qed.
-- 
GitLab