diff --git a/CaseStudies/Gathering/InR2/Weber/Utils.v b/CaseStudies/Gathering/InR2/Weber/Utils.v
index 84629af081a2b81fe9ceb1067653b6866d9aec9a..7d2ded6c40131fbaa4fa8f27b6036de194ec2ed4 100644
--- a/CaseStudies/Gathering/InR2/Weber/Utils.v
+++ b/CaseStudies/Gathering/InR2/Weber/Utils.v
@@ -735,7 +735,7 @@ Ltac pos_R :=
   end.
 
 (* A tactic to push negations in the goal/a hypothesis. *)
-Section PushNegs.
+(*Section PushNegs.
 
 Inductive PNProp :=
   | PNvar (x : nat) 
@@ -743,7 +743,8 @@ Inductive PNProp :=
   | PNfalse 
   | PNnot (a : PNProp) 
   | PNand (a : PNProp) (b : PNProp) 
-  | PNor (a : PNProp) (b : PNProp).
+  | PNor (a : PNProp) (b : PNProp)
+  | PNforall {T : Type} (f : T -> PNProp).
 
 (* Turn a PNProp into a real Prop, assuming interpretations for the variables. *)
 Fixpoint eval_pn (l : list Prop) (p : PNProp) : Prop := 
@@ -754,6 +755,7 @@ Fixpoint eval_pn (l : list Prop) (p : PNProp) : Prop :=
   | PNnot a => ~ eval_pn l a
   | PNand a b => eval_pn l a /\ eval_pn l b
   | PNor a b => eval_pn l a \/ eval_pn l b
+  | PNforall f => forall x, eval_pn l (f x)
   end.
 
 (* Implement push-neg on PNProp. *)
@@ -764,9 +766,10 @@ Fixpoint push_neg_pn (neg : bool) (p : PNProp) : PNProp :=
   | true, PNvar x => PNnot (PNvar x)
   | true, PNtrue => PNfalse 
   | true, PNfalse => PNtrue
-  | true, (PNnot a) => push_neg_pn false a
-  | true, (PNand a b) => PNor (push_neg_pn true a) (push_neg_pn true b)
-  | true, (PNor a b) => PNand (push_neg_pn true a) (push_neg_pn true b) 
+  | true, PNnot a => push_neg_pn false a
+  | true, PNand a b => PNor (push_neg_pn true a) (push_neg_pn true b)
+  | true, PNor a b => PNand (push_neg_pn true a) (push_neg_pn true b) 
+  | true, PNforall f => PNnot (PNforall f)
   | false, PNnot a => push_neg_pn true a
   | false, a => a
   end.
@@ -787,36 +790,43 @@ Ltac list_add a l :=
     end 
   in aux a l O.
 
+Inductive EnvEntry := 
+  | entry : (forall T : Type, T) -> EnvEntry.
+
 (* Turn a Prop into a PNProp. *)
-Ltac reify_aux t l := 
-  lazymatch t with 
-  | True => constr:((PNtrue, l))
-  | False => constr:((PNfalse, l))
+Ltac reify_aux term vars env := 
+  lazymatch term with 
+  | True => constr:((PNtrue, vars))
+  | False => constr:((PNfalse, vars))
   | ~ ?t1 => 
-      match reify_aux t1 l with
-      | (?p1, ?l') => constr:((PNnot p1, l'))
+      match reify_aux t1 vars env with
+      | (?p1, ?vars') => constr:((PNnot p1, vars'))
       end 
   | ?t1 /\ ?t2 => 
-      match reify_aux t1 l with 
-      | (?p1, ?l') => 
-          match reify_aux t2 l' with 
-          | (?p2, ?l'') => constr:((PNand p1 p2, l''))
+      match reify_aux t1 vars env with 
+      | (?p1, ?vars') => 
+          match reify_aux t2 vars' env with 
+          | (?p2, ?vars'') => constr:((PNand p1 p2, vars''))
           end 
       end 
   | ?t1 \/ ?t2 => 
-      match reify_aux t1 l with 
-      | (?p1, ?l') => 
-          match reify_aux t2 l' with 
-          | (?p2, ?l'') => constr:((PNor p1 p2, l''))
+      match reify_aux t1 vars env with 
+      | (?p1, ?vars') => 
+          match reify_aux t2 vars' env with 
+          | (?p2, ?vars'') => constr:((PNor p1 p2, vars''))
           end 
       end 
+  | forall x, ?t1 =>  
+      match reify_aux t1 vars (@cons EnvEntry (@entry T x) env) with 
+      | (?p1, ?vars') => constr:((PNforall (fun x => p1), vars'))
+      end
   | _ => 
       match list_add t l with 
       | (?n, ?l') => constr:((PNvar n, l'))
       end
   end.
 
-Ltac reify t := reify_aux t (@nil Prop).
+Ltac reify t := reify_aux t (@nil Prop) (@nil EnvEntry).
 
 Ltac push_negs := 
   lazymatch goal with 
@@ -825,13 +835,13 @@ Ltac push_negs :=
       | Prop =>
           lazymatch reify P with 
           | (?t, ?l) => 
-              change (eval_pn l t) ; 
-              rewrite pn_correct ; 
-              cbn [eval_pn push_neg_pn nth]
+              change (eval_pn l t)
+              (*rewrite pn_correct ; 
+              cbn [eval_pn push_neg_pn List.nth]*)
           end
       end
   end.
 
 
-Lemma test (A : Prop) (B : nat -> Prop) : ~(A /\ ~B 0%nat).
-Proof. push_negs.
+Lemma test : forall x, x = S x.
+Proof. push_negs.*)
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index ca2569ac5c20bed7940d5faf7123e29c38804d7e..5cbe7723c5fdfecbb531db3c32cc34b35b74fffc 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -1334,14 +1334,115 @@ rewrite Hdist, Hdist'. clear Hdist Hdist'. split.
 Qed.
 
 Lemma deriv_scale (eps : R2) (s : R) : 
-  (deriv (s * eps) = Rabs s * deriv eps)%R.
-Admitted.
+  (0 <= s)%R ->
+  (deriv (s * eps) = s * deriv eps)%R.
+Proof. 
+intros Hs. unfold deriv. 
+rewrite norm_mul, Rabs_right by pos_R.
+rewrite inner_product_mul_l. lra.
+Qed.
+
+Lemma deriv_0 : (deriv 0 = 0)%R.
+Proof.
+unfold deriv. rewrite inner_product_origin_l, norm_origin. lra.
+Qed. 
+
+Lemma deriv_neg_strengthen_1 c : 
+  (0 < c)%R -> 
+  (exists eps, deriv eps < 0)%R ->
+  (exists eps', deriv eps' < 0 /\ norm eps' < c)%R.
+Proof.
+intros Hc [eps Heps].
+assert (Heps_pos : (0 < norm eps)%R).
+{ 
+  case (norm_nonneg eps) as [Hpos | Heq]. 
+  + assumption.
+  + symmetry in Heq. rewrite norm_defined in Heq.
+    rewrite Heq, deriv_0 in Heps. lra.
+}
+
+set (s := (c / (2 * norm eps))%R).
+assert (0 < s)%R by (unfold s ; pos_R).
+
+exists (s * eps)%VS. split.
++ rewrite deriv_scale by pos_R. nra.
++ rewrite norm_mul, Rabs_right by pos_R. 
+  unfold s, Rdiv. rewrite Rinv_mult. repeat rewrite Rmult_assoc.
+  rewrite Rinv_l by lra. lra.
+Qed. 
+
+Lemma deriv_neg_strengthen_2 c d :
+  (0 < c)%R ->
+  (0 < d)%R ->
+  (exists eps, deriv eps < 0)%R -> 
+  (exists eps',
+    deriv eps' < 0 /\
+    norm eps' < c /\
+    deriv eps' + d * Rsqr (norm eps') < 0)%R.
+Proof. 
+intros Hc Hd Heps. apply (@deriv_neg_strengthen_1 (Rmin 1 c)%R) in Heps ; [| pos_R].
+destruct Heps as [eps [Hderiv Hnorm]].
+assert (Heps_pos : (0 < norm eps)%R).
+{ 
+  case (norm_nonneg eps) as [Hpos | Heq]. 
+  + assumption.
+  + symmetry in Heq. rewrite norm_defined in Heq.
+    rewrite Heq, deriv_0 in Hderiv. lra.
+} 
+
+set (s := (-deriv eps / (2 * d * Rsqr (norm eps)))%R).
+assert (Hs_pos : (0 < s)%R) by (unfold s ; pos_R).
+
+set (eps' := (Rmin s 1 * eps)%VS).
+exists eps'. split ; [| split].
++ unfold eps'. rewrite deriv_scale by pos_R.
+  enough (0 < Rmin s 1)%R by nra.
+  pos_R.
++ unfold eps'. rewrite norm_mul. rewrite Rabs_right by pos_R.
+  rewrite <-(Rmult_1_l c).
+  enough (0 < Rmin s 1 <= 1 /\ 0 < norm eps < c)%R by nra.
+  split ; split.
+  - pos_R.
+  - apply Rmin_r.
+  - assumption.
+  - eapply Rlt_le_trans ; [apply Hnorm | apply Rmin_r].
++ enough (d * Rsqr (norm eps') < -deriv eps')%R by lra.
+  unfold eps'. rewrite deriv_scale by pos_R.
+  rewrite norm_mul, Rabs_right by pos_R.
+  rewrite R_sqr.Rsqr_mult. unfold Rsqr at 1. repeat rewrite <-Rmult_assoc.
+  rewrite (Rmult_comm d). repeat rewrite Rmult_assoc. rewrite Ropp_mult_distr_r.
+  apply Rmult_lt_compat_l ; [pos_R |].
+  rewrite <-Rmult_assoc, (Rmult_comm d), Rmult_assoc. 
+  apply (@Rlt_le_trans _ ((- deriv eps / (d * (norm eps)²)) * (d * Rsqr (norm eps)))%R).
+  - apply Rmult_lt_compat_r ; [pos_R |].
+    eapply Rle_lt_trans ; [apply Rmin_l |].
+    enough (Hrw : (- deriv eps / (d * (norm eps)²) = 2 * s)%R).
+    { rewrite Hrw. lra. }
+    unfold s, Rdiv. repeat rewrite Rinv_mult. repeat rewrite <-Rmult_assoc.
+    rewrite (Rmult_comm 2). repeat rewrite Rmult_assoc. f_equal.
+    repeat rewrite <-Rmult_assoc. rewrite Rinv_r by lra. lra.
+  - unfold Rdiv. rewrite Rmult_assoc, Rinv_l.
+    * lra.
+    * enough (0 < d * Rsqr (norm eps))%R by lra. pos_R. 
+Qed.
 
 (* If we can find a direction eps such that deriv eps < 0, 
  * then w is not a weber point. *)
 Lemma deriv_neg_not_weber : 
   (exists eps, deriv eps < 0)%R -> ~Weber ps w.
-Proof. Admitted.
+Proof.
+destruct dist_sum_bound as [c [d [Hc [Hd Hbound]]]]. intros Heps.
+destruct (deriv_neg_strengthen_2 Hc Hd Heps) as [eps [Hderiv [Hnorm Hsum]]].
+assert (Hdist : (dist_sum ps (w + eps) < dist_sum ps w)%R).
+{  
+  destruct (Hbound eps Hnorm) as [Hbound' _].
+  eapply Rle_lt_trans ; [exact Hbound' |].
+  rewrite <-(Rplus_0_r (dist_sum ps w)) at 2. repeat rewrite Rplus_assoc.
+  apply Rplus_lt_compat_l. assumption.
+}
+unfold Weber, argmin. apply Classical_Pred_Type.ex_not_not_all.
+exists (w + eps)%VS. lra.
+Qed.
 
 (* If we cannot find a direction eps such that deriv eps < 0,
  * then w is a local minimum for dist_sum ps. *)