diff --git a/FEM/Algebra/AffineSpace_new.v b/FEM/Algebra/AffineSpace_new.v
index 377e9ee153846713887adeda026ae0cb88884743..43009282fa7e746183067ee643ea16dbab9f5c22 100644
--- a/FEM/Algebra/AffineSpace_new.v
+++ b/FEM/Algebra/AffineSpace_new.v
@@ -2701,23 +2701,6 @@ Proof.
 move=>> [n [L [B [HL [HB HA]]]]]; rewrite HA; apply Barycenter_closure; easy.
 Qed.
 
-(* FIXME: how to destruct H? *)
-Lemma barycenter_closure_EX :
-  forall (gen : E -> Prop) A,
-    barycenter_closure' gen A ->
-    { n & { LB : 'K^n * 'E^n | let (L, B) := LB in
-      sum L = 1 /\ (forall i, L i <> 0) /\ inclF B gen /\ A = barycenter L B } }.
-Proof.
-intros gen A [n [LB H]].
-
-intros gen A HA; induction HA. as [n L B HL HB].
-destruct (barycenter_normalized_n0_EX L B HL)
-    as [n1 [L1 [A1 [HL1a [HL1b [HA1a HA1b]]]]]].
-exists n1, L1, A1; repeat split; try easy.
-apply (inclF_monot_l _ B); easy.
-Qed.
-
-(*
 Lemma barycenter_closure_ex_rev :
   forall (gen : E -> Prop) A,
     barycenter_closure gen A ->
@@ -2730,7 +2713,19 @@ destruct (barycenter_normalized_n0_ex L B HL)
 exists n1, L1, A1; repeat split; try easy.
 apply (inclF_monot_l _ B); easy.
 Qed.
-*)
+
+Lemma barycenter_closure'_EX :
+  forall (gen : E -> Prop) A,
+    barycenter_closure' gen A ->
+    { n & { LB : 'K^n * 'E^n | let (L, B) := LB in
+      sum L = 1 /\ (forall i, L i <> 0) /\ inclF B gen /\ A = barycenter L B } }.
+Proof.
+intros gen A [n [[L B] [HL [HB HA]]]]; subst.
+destruct (barycenter_normalized_n0_EX L B HL)
+    as [n1 [[L1 A1] [HL1a [HL1b [HA11 HA1b]]]]].
+exists n1, (L1, A1); repeat split; try easy.
+apply (inclF_monot_l _ B); easy.
+Qed.
 
 Lemma bc_len_EX :
   forall (gen : E -> Prop) A,
@@ -2746,6 +2741,21 @@ exists n; intros _; exists L, B; easy.
 exists 0; intros HA'; easy.
 Qed.
 
+(* FIXME: we need to decide whether A is in the barycenter_closure' or not...  *)
+Lemma bc_len'_EX :
+  forall (gen : E -> Prop) A,
+    { n & barycenter_closure' gen A ->
+      { LB : 'K^n * 'E^n | let (L, B) := LB in
+        sum L = 1 /\ (forall i, L i <> 0) /\
+        inclF B gen /\ A = barycenter L B } }.
+Proof.
+intros gen A.
+destruct (classic_dec (barycenter_closure' gen A)) as [HA | HA].
+destruct (barycenter_closure'_EX _ _ HA) as [n [L [B HLB]]].
+exists n; intros _; exists L, B; easy.
+exists 0; intros HA'; easy.
+Qed.
+
 Definition bc_len (gen : E -> Prop) A := proj1_sig (bc_len_EX gen A).
 
 Lemma bc_EX :