From 12607acaaeba346a5325eba7705b35cc456a636e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 18 Mar 2024 19:20:25 +0100
Subject: [PATCH] Make it strong!
---
FEM/Algebra/AffineSpace_new.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/FEM/Algebra/AffineSpace_new.v b/FEM/Algebra/AffineSpace_new.v
index bcbedc16..377e9ee1 100644
--- a/FEM/Algebra/AffineSpace_new.v
+++ b/FEM/Algebra/AffineSpace_new.v
@@ -215,7 +215,8 @@ Context {E : AffineSpace V}.
Lemma transl_EX :
{ f | forall (A : E), cancel (vect A) (f A) /\ cancel (f A) (vect A) }.
Proof.
-assert (H : forall A : E, exists ! f, cancel (vect A) f /\ cancel f (vect A)).
+assert (H : forall A : E, { f | unique (fun g => cancel (vect A) g /\ cancel g (vect A)) f }).
+ intros A; destruct (vect_l_bij_EX )
intros A; destruct (vect_l_bij A) as [f Hf1 Hf2]; exists f; split; [easy |].
intros f' [Hf'1 Hf'2]; apply fun_ext; intros u.
apply (vect_l_inj A); rewrite Hf2 Hf'2; easy.
--
GitLab