diff --git a/CaseStudies/Gathering/InR2/Weber/Utils.v b/CaseStudies/Gathering/InR2/Weber/Utils.v
index c8bb842be67e6885abad889fd32fce056643fb10..84629af081a2b81fe9ceb1067653b6866d9aec9a 100644
--- a/CaseStudies/Gathering/InR2/Weber/Utils.v
+++ b/CaseStudies/Gathering/InR2/Weber/Utils.v
@@ -18,7 +18,7 @@
 Require Import Bool.
 Require Import Arith.Div2.
 Require Import Lia Field.
-Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def.
+Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def Ranalysis.
 Require Import List.
 Require Import SetoidList.
 Require Import Relations.
@@ -69,7 +69,7 @@ Ltac change_RHS E :=
                           ____
                           Q
   After completing this proof, Q becomes a hypothesis in the context. *)
-  Ltac feed H :=
+Ltac feed H :=
   match type of H with
   | ?foo -> _ =>
     let FOO := fresh in
@@ -659,3 +659,179 @@ case (Nat.Even_or_Odd n) as [[k ->] | [k ->]].
 + rewrite Nat.add_1_r, Nat.div2_succ_double. lia.
 + rewrite 2 Nat.add_1_r. cbn -[Nat.mul]. rewrite Nat.div2_double. lia.
 Qed.
+
+Lemma Rmin_nonneg (x y : R) : (0 <= x)%R -> (0 <= y)%R -> (0 <= Rmin x y)%R.
+Proof. intros. unfold Rmin. destruct (Rle_dec x y) ; assumption. Qed.
+
+Lemma Rmax_nonneg_left (x y : R) : (0 <= x)%R -> (0 <= Rmax x y)%R.
+Proof. intros. transitivity x ; [assumption | apply Rmax_l]. Qed.
+
+Lemma Rmax_nonneg_right (x y : R) : (0 <= y)%R -> (0 <= Rmax x y)%R.
+Proof. intros. transitivity y ; [assumption | apply Rmax_r]. Qed.
+
+Lemma Rmax_pos_left (x y : R) : (0 < x)%R -> (0 < Rmax x y)%R.
+Proof. intros. apply (Rlt_le_trans _ x) ; [assumption | apply Rmax_l]. Qed.
+
+Lemma Rmax_pos_right (x y : R) : (0 < y)%R -> (0 < Rmax x y)%R.
+Proof. intros. apply (Rlt_le_trans _ y) ; [assumption | apply Rmax_r]. Qed.
+
+Ltac pos_R_close := solve [ easy | lra | nra | lia | nia ].
+
+(* Attempt to prove a goal of the form 0%R < ?X or 0%R <= ?X. *)
+(* This either fails or succeeds completely (i.e. it does not leave any subgoal open). *)
+(* If you have inequalities you would want pos_R to use, consider using generalize before pos_R. *)
+Ltac pos_R :=
+  match goal with 
+  (* Using hypotheses. *)
+  | [ |- _ -> _] => intros ; pos_R
+  | [ H : ?P |- ?P ] => exact H
+  (* Change Rgt/Rge to Rlt/Rle. *)
+  | [ |- (_ > _)%R ] => apply Rlt_gt ; pos_R
+  | [ |- (_ >= _)%R ] => apply Rle_ge ; pos_R
+  (* Addition. *)
+  | [ |- (0 < ?X + ?Y)%R ] => 
+    solve [ apply Rplus_lt_0_compat ; pos_R
+          | apply Rplus_lt_le_0_compat ; pos_R
+          | apply Rplus_le_lt_0_compat ; pos_R ]
+  | [ |- (0 <= ?X + ?Y)%R ] => apply Rplus_le_le_0_compat ; pos_R
+  (* Multiplication. *)
+  | [ |- (0 < ?X * ?Y)%R ] => apply Rmult_lt_0_compat ; pos_R
+  | [ |- (0 <= ?X * ?Y)%R ] => apply Rmult_le_pos ; pos_R
+  (* Inverse. *)
+  | [ |- (0 < / _)%R ] => apply Rinv_0_lt_compat ; pos_R
+  (* Division. *)
+  | [ |- (0 < _ / _)%R ] => apply Rdiv_lt_0_compat ; pos_R
+  | [ |- (0 <= _ / _)%R ] => apply Rdiv_le_0_compat ; pos_R
+  (* Square. *)
+  | [ |- (0 < Rsqr _)%R ] => apply Rlt_0_sqr ; pos_R_close
+  | [ |- (0 <= Rsqr _)%R ] => apply Rle_0_sqr ; pos_R_close
+  (* Absolute value. *)
+  | [ |- (0 < Rabs _)%R ] => apply Rabs_pos_lt ; pos_R_close
+  | [ |- (0 <= Rabs _)%R ] => apply Rabs_pos ; pos_R_close
+  (* Norm. *)
+  | [ |- (0 <= norm _)%R ] => apply norm_nonneg ; pos_R_close
+  (* Distance. *)
+  | [ |- (0 <= dist _ _)%R ] => apply dist_nonneg ; pos_R_close
+  (* Exponential. *)
+  | [ |- (0 < exp _)%R ] => apply exp_pos ; pos_R_close
+  | [ |- (0 <= exp _)%R ] => apply Rlt_le, exp_pos ; pos_R_close
+  (* INR. *)
+  | [ |- (0 < INR _)%R ] => apply lt_0_INR ; pos_R_close
+  | [ |- (0 <= INR _)%R ] => apply pos_INR ; pos_R_close
+  (* Minimum. *)
+  | [ |- (0 < Rmin _ _)%R ] => apply Rmin_pos ; pos_R
+  | [ |- (0 <= Rmin _ _)%R ] => apply Rmin_nonneg ; pos_R
+  (* Maximum. *)
+  | [ |- (0 < Rmax _ _)%R ] => 
+      solve [ apply Rmax_pos_left ; pos_R
+            | apply Rmax_pos_right ; pos_R ]
+  | [ |- (0 <= Rmax _ _)%R ] => 
+      solve [ apply Rmax_nonneg_left ; pos_R
+            | apply Rmax_nonneg_right ; pos_R ]
+  (* Strengthen Rle to Rlt. *)
+  | [ |- (_ <= _)%R ] => apply Rlt_le ; pos_R
+  (* Try to close the goal with lra/nra. *)
+  | _ => pos_R_close
+  end.
+
+(* A tactic to push negations in the goal/a hypothesis. *)
+Section PushNegs.
+
+Inductive PNProp :=
+  | PNvar (x : nat) 
+  | PNtrue  
+  | PNfalse 
+  | PNnot (a : PNProp) 
+  | PNand (a : PNProp) (b : PNProp) 
+  | PNor (a : PNProp) (b : PNProp).
+
+(* Turn a PNProp into a real Prop, assuming interpretations for the variables. *)
+Fixpoint eval_pn (l : list Prop) (p : PNProp) : Prop := 
+  match p with 
+  | PNvar x => List.nth x l True
+  | PNtrue => True 
+  | PNfalse => False 
+  | 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
+  end.
+
+(* Implement push-neg on PNProp. *)
+(* The bool parameter determines the formula we are working on : 
+ * [p] (when neg = false) or [PNnot p] (when neg = true). *)
+Fixpoint push_neg_pn (neg : bool) (p : PNProp) : PNProp := 
+  match neg, p with 
+  | 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) 
+  | false, PNnot a => push_neg_pn true a
+  | false, a => a
+  end.
+
+Lemma pn_correct p l :
+  (eval_pn l p <-> eval_pn l (push_neg_pn false p)).
+Proof. Admitted.
+
+Ltac list_add a l :=
+  let rec aux a l n :=
+    lazymatch l with
+    | nil => constr:((n, List.cons a l))
+    | a :: _ => constr :((n, l))
+    | ?x :: ?l =>
+        match aux a l (S n) with
+        | (?n , ?l) => constr:((n, List.cons x l))
+        end
+    end 
+  in aux a l O.
+
+(* Turn a Prop into a PNProp. *)
+Ltac reify_aux t l := 
+  lazymatch t with 
+  | True => constr:((PNtrue, l))
+  | False => constr:((PNfalse, l))
+  | ~ ?t1 => 
+      match reify_aux t1 l with
+      | (?p1, ?l') => constr:((PNnot p1, l'))
+      end 
+  | ?t1 /\ ?t2 => 
+      match reify_aux t1 l with 
+      | (?p1, ?l') => 
+          match reify_aux t2 l' with 
+          | (?p2, ?l'') => constr:((PNand p1 p2, l''))
+          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''))
+          end 
+      end 
+  | _ => 
+      match list_add t l with 
+      | (?n, ?l') => constr:((PNvar n, l'))
+      end
+  end.
+
+Ltac reify t := reify_aux t (@nil Prop).
+
+Ltac push_negs := 
+  lazymatch goal with 
+  | [ |- ?P ] => 
+      lazymatch type of P with 
+      | Prop =>
+          lazymatch reify P with 
+          | (?t, ?l) => 
+              change (eval_pn l t) ; 
+              rewrite pn_correct ; 
+              cbn [eval_pn push_neg_pn nth]
+          end
+      end
+  end.
+
+
+Lemma test (A : Prop) (B : nat -> Prop) : ~(A /\ ~B 0%nat).
+Proof. push_negs.
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 003e3b39952eeb8fb9dfe8f0fad087bd15f20b63..ca2569ac5c20bed7940d5faf7123e29c38804d7e 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -717,80 +717,6 @@ Proof. Admitted.
 
 Section WeberFirstOrder.
 
-Lemma Rmin_nonneg (x y : R) : (0 <= x)%R -> (0 <= y)%R -> (0 <= Rmin x y)%R.
-Proof. intros. unfold Rmin. destruct (Rle_dec x y) ; assumption. Qed.
-
-Lemma Rmax_nonneg_left (x y : R) : (0 <= x)%R -> (0 <= Rmax x y)%R.
-Proof. intros. transitivity x ; [assumption | apply Rmax_l]. Qed.
-
-Lemma Rmax_nonneg_right (x y : R) : (0 <= y)%R -> (0 <= Rmax x y)%R.
-Proof. intros. transitivity y ; [assumption | apply Rmax_r]. Qed.
-
-Lemma Rmax_pos_left (x y : R) : (0 < x)%R -> (0 < Rmax x y)%R.
-Proof. intros. apply (Rlt_le_trans _ x) ; [assumption | apply Rmax_l]. Qed.
-
-Lemma Rmax_pos_right (x y : R) : (0 < y)%R -> (0 < Rmax x y)%R.
-Proof. intros. apply (Rlt_le_trans _ y) ; [assumption | apply Rmax_r]. Qed.
-
-Ltac pos_R_close := solve [ easy | lra | nra | lia | nia ].
-
-(* Attempt to prove a goal of the form 0%R < ?X or 0%R <= ?X. *)
-(* This either fails or succeeds completely (i.e. it does not leave any subgoal open). *)
-(* If you have inequalities you would want pos_R to use, consider using generalize before pos_R. *)
-Ltac pos_R :=
-  match goal with 
-  (* Using hypotheses. *)
-  | [ |- _ -> _] => intros ; pos_R
-  | [ H : ?P |- ?P ] => exact H
-  (* Change Rgt/Rge to Rlt/Rle. *)
-  | [ |- (_ > _)%R ] => apply Rlt_gt ; pos_R
-  | [ |- (_ >= _)%R ] => apply Rle_ge ; pos_R
-  (* Addition. *)
-  | [ |- (0 < ?X + ?Y)%R ] => 
-    solve [ apply Rplus_lt_0_compat ; pos_R
-          | apply Rplus_lt_le_0_compat ; pos_R
-          | apply Rplus_le_lt_0_compat ; pos_R ]
-  | [ |- (0 <= ?X + ?Y)%R ] => apply Rplus_le_le_0_compat ; pos_R
-  (* Multiplication. *)
-  | [ |- (0 < ?X * ?Y)%R ] => apply Rmult_lt_0_compat ; pos_R
-  | [ |- (0 <= ?X * ?Y)%R ] => apply Rmult_le_pos ; pos_R
-  (* Inverse. *)
-  | [ |- (0 < / _)%R ] => apply Rinv_0_lt_compat ; pos_R
-  (* Division. *)
-  | [ |- (0 < _ / _)%R ] => apply Rdiv_lt_0_compat ; pos_R
-  | [ |- (0 <= _ / _)%R ] => apply Rdiv_le_0_compat ; pos_R
-  (* Square. *)
-  | [ |- (0 < Rsqr _)%R ] => apply Rlt_0_sqr ; pos_R_close
-  | [ |- (0 <= Rsqr _)%R ] => apply Rle_0_sqr ; pos_R_close
-  (* Absolute value. *)
-  | [ |- (0 < Rabs _)%R ] => apply Rabs_pos_lt ; pos_R_close
-  | [ |- (0 <= Rabs _)%R ] => apply Rabs_pos ; pos_R_close
-  (* Norm. *)
-  | [ |- (0 <= norm _)%R ] => apply norm_nonneg ; pos_R_close
-  (* Distance. *)
-  | [ |- (0 <= dist _ _)%R ] => apply dist_nonneg ; pos_R_close
-  (* Exponential. *)
-  | [ |- (0 < exp _)%R ] => apply exp_pos ; pos_R_close
-  | [ |- (0 <= exp _)%R ] => apply Rlt_le, exp_pos ; pos_R_close
-  (* INR. *)
-  | [ |- (0 < INR _)%R ] => apply lt_0_INR ; pos_R_close
-  | [ |- (0 <= INR _)%R ] => apply pos_INR ; pos_R_close
-  (* Minimum. *)
-  | [ |- (0 < Rmin _ _)%R ] => apply Rmin_pos ; pos_R
-  | [ |- (0 <= Rmin _ _)%R ] => apply Rmin_nonneg ; pos_R
-  (* Maximum. *)
-  | [ |- (0 < Rmax _ _)%R ] => 
-      solve [ apply Rmax_pos_left ; pos_R
-            | apply Rmax_pos_right ; pos_R ]
-  | [ |- (0 <= Rmax _ _)%R ] => 
-      solve [ apply Rmax_nonneg_left ; pos_R
-            | apply Rmax_nonneg_right ; pos_R ]
-  (* Strengthen Rle to Rlt. *)
-  | [ |- (_ <= _)%R ] => apply Rlt_le ; pos_R
-  (* Try to close the goal with lra/nra. *)
-  | _ => pos_R_close
-  end.
-
 Variables (w : R2) (ps : list R2).
 
 (* The points in ps that are not equal to w. *)
@@ -1411,25 +1337,25 @@ Lemma deriv_scale (eps : R2) (s : R) :
   (deriv (s * eps) = Rabs s * deriv eps)%R.
 Admitted.
 
-Lemma deriv_neg_not_weber (eps : R2) : 
-  (deriv eps < 0)%R -> not (Weber ps w).
+(* 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.
 
+(* If we cannot find a direction eps such that deriv eps < 0,
+ * then w is a local minimum for dist_sum ps. *)
+Lemma deriv_nonneg_local_min :
+  (forall eps, deriv eps >= 0)%R -> 
+  exists c, 
+    (0 < c)%R /\ 
+    forall eps, (norm eps < c)%R -> (dist_sum ps w <= dist_sum ps (w + eps))%R.
+Proof. Admitted.
 
-Lemma candidate_exists_not_weber :
-  (exists eps, eps <> 0%VS /\ candidate eps) -> not (Weber ps w).
-Proof. 
-(* Show that dist_sum (w + s * eps) < dist_sum w for some positive small s. *)  
-Admitted.
-
-Lemma no_candidate_weber :
-  (forall eps, eps <> 0%VS -> not (candidate eps)) -> Weber ps w.
-Proof.
-Admitted.
-
-(* This should be a consequence of the cauchy-schwartz inequality. *)
-Lemma candidate_exists_iff : 
-  (norm (list_sumVS (List.map u ps)) > INR (mult w))%R <-> exists eps, eps <> 0%VS /\ candidate eps.
+ 
+(* This is a consequence of the cauchy-schwartz inequality. *)
+Lemma deriv_neg_iff : 
+  (norm (list_sumVS (List.map u ps)) > INR (mult w))%R <-> (exists eps, deriv eps < 0)%R.
 Admitted.
 
 (* This is the first order condition for weber points. *)