diff --git a/CaseStudies/Gathering/InR2/Weber/Utils.v b/CaseStudies/Gathering/InR2/Weber/Utils.v
index 23687ba9dd97962d9b7b47867ab0d57c8d9f34d2..9744c6cefad52fd5d99e14f3da717d2cbd7c6141 100644
--- a/CaseStudies/Gathering/InR2/Weber/Utils.v
+++ b/CaseStudies/Gathering/InR2/Weber/Utils.v
@@ -224,7 +224,7 @@ intros HF HE. induction HF as [| x x' l l' Hxx' Hll' IH].
   destruct HE as [Dxx' | HE].
   - destruct Hxx' as [Exx' | Ex'w] ; intuition.
     rewrite Ex'w in Dxx' |- *. cbn -[equiv].
-    repeat destruct_match ; intuition. apply le_lt_n_Sm. now apply countA_occ_le.
+    repeat destruct_match ; intuition. rewrite Nat.lt_succ_r. now apply countA_occ_le.
   - destruct Hxx' as [Exx' | Ex'w] ; cbn -[equiv] ; repeat destruct_match ; intuition.
     rewrite Exx', e in *. intuition.
 Qed.
@@ -735,426 +735,71 @@ Ltac pos_R :=
   | _ => pos_R_close
   end.
 
-(* A tactic to rearrange operands of associative and commutative operations. *)
-(*
-Class ACOp {T : Type} (op : T -> T -> T) :=
-  {
-    op_comm : forall a b, op a b = op b a ;
-    op_assoc : forall a b c, op a (op b c) = op (op a b) c ;
-  }.
-
-Inductive tree T := 
-  | Leaf : T -> tree T
-  | Node : tree T -> tree T -> tree T.
-
-Fixpoint eval T (op : T -> T -> T) (t : tree T) : T :=
-  match t with 
-  | Leaf x => x
-  | Node t1 t2 => op (eval op t1) (eval op t2) 
-  end.
-
-Fixpoint size {T} (t : tree T) : nat := 
-  match t with 
-  | Leaf _ => 1 
-  | Node t1 t2 => size t1 + size t2
-  end.
-
-Lemma size_pos {T} (t : tree T) : 0 < size t.
-Proof. induction t as [v | t1 IH1 t2 IH2] ; simpl ; lia. Qed.
-
-Fixpoint extract {T} (t : tree T) (i : nat) : T * option (tree T) := 
-  match t with 
-  | Leaf x => (x, None)
-  | Node t1 t2 => 
-    if lt_dec i (size t1) then 
-      match extract t1 i with 
-      | (x, None) => (x, Some t2)
-      | (x, Some t1') => (x, Some (Node t1' t2))
-      end
-    else 
-      match extract t2 (i - size t1) with 
-      | (y, None) => (y, Some t1)
-      | (y, Some t2') => (y, Some (Node t1 t2'))
-      end
-  end.
-
-Lemma extract_None {T} (op : T -> T -> T) x t i : 
-  extract t i = (x, None) -> eval op t = x.
-Proof. 
-case t as [v | t1 t2].
-+ simpl. intros H ; inversion H. reflexivity.
-+ simpl. case (lt_dec i (size t1)).
-  - case (extract t1 i) as [x1 [t1' |]] ; discriminate.
-  - case (extract t2 (i - size t1)) as [x2 [t2' |]] ; discriminate.
-Qed.
-
-Lemma extract_Some {T} (op : T -> T -> T) `{AC : ACOp T op} x t t' i : 
-  extract t i = (x, Some t') -> eval op t = op x (eval op t').
-Proof.
-set (AC' := AC). destruct AC as [comm assoc]. 
-revert i x t'. induction t as [v | t1 IH1 t2 IH2] ; intros i x t'.
-+ simpl. discriminate.
-+ simpl. case (lt_dec i (size t1)) as [Hi | Hi].
-  - case (extract t1 i) as [x1 [t1' |]] eqn:Ht1.
-    * intros H ; inversion H ; subst ; clear H. simpl.
-      specialize (IH1 _ _ _ Ht1). rewrite IH1, assoc. reflexivity.
-    * intros H ; inversion H ; subst ; clear H.
-      apply (extract_None op) in Ht1. rewrite Ht1.
-      reflexivity.
-  - case (extract t2 (i - size t1)) as [x2 [t2' |]] eqn:Ht2.
-    * intros H ; inversion H ; subst ; clear H. simpl. 
-      specialize (IH2 _ _ _ Ht2). rewrite IH2.
-      rewrite assoc, (comm _ x), <-assoc. reflexivity.
-    * intros H ; inversion H ; subst ; clear H.
-      apply (extract_None op) in Ht2. rewrite Ht2.
-      rewrite comm. reflexivity.
-Qed. 
+Ltac simp_fct := 
+  cbv [fct_cte Ranalysis1.id Ranalysis1.comp plus_fct mult_fct inv_fct div_fct].
 
-Lemma extract_size {T} x (t t' : tree T) i : 
-  extract t i = (x, Some t') -> size t' < size t.
+Local Instance derivable_pt_lim_compat : Proper ((equiv ==> equiv) ==> equiv ==> equiv ==> iff) derivable_pt_lim.
 Proof.
-revert i x t'. induction t as [v | t1 IH1 t2 IH2] ; intros i x t'.
-+ simpl. discriminate.
-+ simpl. case (lt_dec i (size t1)) as [Hi | Hi].
-  - case (extract t1 i) as [x1 [t1' |]] eqn:Ht1.
-    * intros H ; inversion H ; subst ; clear H. simpl.
-      specialize (IH1 _ _ _ Ht1). lia. 
-    * intros H ; inversion H ; subst ; clear H.
-      generalize (size_pos t1). lia.
-  - case (extract t2 (i - size t1)) as [x2 [t2' |]] eqn:Ht2.
-    * intros H ; inversion H ; subst ; clear H. simpl. 
-      specialize (IH2 _ _ _ Ht2). lia.
-    * intros H ; inversion H ; subst ; clear H.
-      generalize (size_pos t2). lia.
-Qed.
-
-Fixpoint insert {T} (t : tree T) (i : nat) (v : T) : tree T := 
-  match t with 
-  | Leaf x => 
-    if le_dec i 0 then 
-      Node (Leaf v) (Leaf x) 
-    else 
-      Node (Leaf x) (Leaf v)
-  | Node t1 t2 => 
-    if lt_dec i (size t1) then 
-      Node (insert t1 i v) t2  
-    else 
-      Node t1 (insert t2 (i - size t1) v)
-  end.
-
-Lemma insert_correct {T} (op : T -> T -> T) `{AC : ACOp T op} t i v : 
-  eval op (insert t i v) = op v (eval op t).
-Proof.
-destruct AC as [comm assoc].
-revert i ; induction t as [x | t1 IH1 t2 IH2] ; intros i.
-+ simpl. case (le_dec i 0) as [_ | _] ; simpl.
-  - reflexivity.
-  - now rewrite comm.
-+ simpl. case (lt_dec i (size t1)) as [_ | _] ; simpl.
-  - now rewrite IH1, assoc.
-  - rewrite IH2. rewrite assoc, (comm _ v), <-assoc. reflexivity.
-Qed.      
-
-Definition move2 {T} (t : tree T) (i j : nat) : tree T := 
-  if lt_dec i j then 
-    match extract t i with 
-    | (x, None) => Leaf x
-    | (x, Some t') => insert t' (j - 1) x
-    end
-  else 
-    match extract t i with 
-    | (x, None) => Leaf x
-    | (x, Some t') => insert t' j x
-    end.
-
-Lemma move2_correct {T} (op : T -> T -> T) `{AC : ACOp T op} t i j :
-  eval op (move2 t i j) = eval op t.
+intros f1 f2 Hf x1 x2 Hx l1 l2 Hl. unfold derivable_pt_lim. split.
++ intros H eps Heps. destruct (H eps Heps) as [delta H']. exists delta.
+  intros h. rewrite <-Hl, <-Hx. rewrite <-(Hf _ _ (eq_refl x1)), <-(Hf _ _ (eq_refl (x1 + h)%R)).
+  now apply H'.
++ intros H eps Heps. destruct (H eps Heps) as [delta H']. exists delta.
+  intros h. rewrite Hl, Hx. rewrite (Hf _ _ (eq_refl x2)), (Hf _ _ (eq_refl (x2 + h)%R)).
+  now apply H'.
+Qed.
+
+Lemma derivable_pt_lim_inv :
+  forall (f : R -> R) (x l : R),
+    derivable_pt_lim f x l ->
+    f x <> 0%R ->
+    derivable_pt_lim (/ f) x ((- l) / Rsqr (f x))%R.
 Proof.
-unfold move2. case (lt_dec i j) as [_ | _].
-+ case (extract t i) as [x [t' |]] eqn:H.
-  - apply (@extract_Some _ op) in H ; [|assumption].
-    rewrite H. rewrite insert_correct by assumption. 
-    reflexivity.
-  - apply (@extract_None _ op) in H. rewrite H. reflexivity.
-+ case (extract t i) as [x [t' |]] eqn:H.   
-  - apply (@extract_Some _ op) in H ; [|assumption].
-    rewrite H. rewrite insert_correct by assumption. 
-    reflexivity.
-  - apply (@extract_None _ op) in H. rewrite H. reflexivity.
-Qed.
-
-Program Fixpoint assoc_right {T} (t : tree T) { measure (size t) } : tree T :=
-  match extract t 0 with 
-  | (x, None) => Leaf x 
-  | (x, Some t') => Node (Leaf x) (assoc_right t')
-  end.
-Next Obligation.
-eapply extract_size ; eauto.
-Qed.
-
-Lemma assoc_right_def {T} (t : tree T) :
-  assoc_right t = 
-    match extract t 0 with 
-    | (x, None) => Leaf x 
-    | (x, Some t') => Node (Leaf x) (assoc_right t')
-    end.
-Proof. 
-Admitted.
-
-Lemma assoc_right_correct {T} (op : T -> T -> T) `{AC : ACOp T op} (t : tree T) :
-  eval op (assoc_right t) = eval op t.
-Proof.
-induction t using (well_founded_induction (wf_inverse_image _ nat _ (@size _) PeanoNat.Nat.lt_wf_0)).
-rewrite assoc_right_def.
-case (extract t 0) as [x [t' |]] eqn:Hextract.
-+ simpl. specialize (H _ (extract_size _ _ Hextract)).
-  rewrite H. apply (@extract_Some _ op _) in Hextract.
-  now rewrite Hextract.
-+ simpl. apply (extract_None op) in Hextract. now rewrite Hextract.
-Qed. 
-
-Fixpoint reverse {T} (t : tree T) : tree T :=
-  match t with 
-  | Leaf x => Leaf x 
-  | Node t1 t2 => Node (reverse t2) (reverse t1)
-  end.
-
-Lemma reverse_correct {T} (op : T -> T -> T) `{AC : ACOp T op} (t : tree T) :
-  eval op (reverse t) = eval op t.
-Proof.
-destruct AC as [comm assoc].
-induction t as [x | t1 IH1 t2 IH2] ; simpl.
+intros f x l Hderiv Hf. 
+assert (Hdiv := derivable_pt_lim_div (fct_cte 1%R) f x 0%R l). feed_n 3 Hdiv.
+{ apply derivable_pt_lim_const. }
+{ assumption. }
+{ lra. }
+revert Hdiv. apply derivable_pt_lim_compat.
++ intros x1 x2 Hx. simp_fct. simpl. rewrite Hx. lra.
 + reflexivity.
-+ rewrite IH1, IH2, comm. reflexivity.
-Qed.
-
-Definition assoc_left {T} (t : tree T) := reverse (assoc_right (reverse t)).
-
-Lemma assoc_left_correct {T} (op : T -> T -> T) `{AC : ACOp T op} (t : tree T) :
-  eval op (assoc_left t) = eval op t.
-Proof.
-unfold assoc_left.
-rewrite reverse_correct, assoc_right_correct, reverse_correct by assumption.
-reflexivity.
-Qed.
-
-(* Turn a T into a list T. *)
-Ltac reify T op term := 
-  lazymatch term with 
-  | op ?x ?y => 
-      lazymatch reify T op x with 
-      | ?t1 => 
-          lazymatch reify T op y with 
-          | ?t2 => constr:(@Node T t1 t2)
-          end 
-      end 
-  | ?x => constr:(@Leaf T x)
-  end.
-
-Ltac reify_lhs op := 
-  lazymatch type of op with
-  | ?T -> ?T -> ?T => 
-    lazymatch goal with 
-    | [ |- ?eq ?lhs ?rhs ] =>
-      lazymatch type of eq with 
-      | T -> T -> _ =>  
-        lazymatch reify T op lhs with 
-        | ?t => change (eq (eval op t) rhs)
-        end
-      end
-    end
-  | _ => fail "reify_lhs: expected a binary operator of type T -> T -> T for some T : Type"
-  end.
-
-Ltac reify_rhs op := 
-  lazymatch type of op with
-  | ?T -> ?T -> ?T => 
-    lazymatch goal with 
-    | [ |- ?eq ?lhs ?rhs ] =>
-      lazymatch type of eq with 
-      | T -> T -> _ =>  
-        lazymatch reify T op rhs with 
-        | ?t => change (eq lhs (eval op t))
-        end
-      end
-    end
-  | _ => fail "reify_rhs: expected a binary operator of type T -> T -> T for some T : Type"
-  end.
-  
-
-(* Move. *)
-
-Ltac move_lhs op i j :=
-  reify_lhs op ; 
-  rewrite <-(@move2_correct _ op _ _ i j).
-
-Ltac move_rhs op i j :=
-  reify_rhs op ; 
-  rewrite <-(@move2_correct _ op _ _ i j).
-
-(* Assoc right. *)
-  
-Ltac assoc_right_lhs op :=
-  reify_lhs op ;
-  rewrite <-(@assoc_right_correct _ op _ _).
-
-Ltac assoc_right_rhs op :=
-  reify_rhs op ;
-  rewrite <-(@assoc_right_correct _ op _ _).
-
-Ltac assoc_right op := assoc_right_rhs op ; assoc_right_lhs op.
-
-(* Assoc left. *)
-
-Ltac assoc_left_lhs op :=
-  reify_lhs op ;
-  rewrite <-(@assoc_left_correct _ op _ _).
-
-Ltac assoc_left_rhs op :=
-  reify_rhs op ;
-  rewrite <-(@assoc_left_correct _ op _ _).
-
-Ltac assoc_left op := assoc_left_rhs op ; assoc_left_lhs op.
-
-(* A couple of standard instances. *)
-
-#[export] Instance nat_add_ac : ACOp Nat.add.
-Proof. constructor ; intros ; lia. Qed.
-
-#[export] Instance nat_mul_ac : ACOp Nat.mul.
-Proof. constructor ; intros ; lia. Qed.
-
-#[export] Instance rplus_ac : ACOp Rplus.
-Proof. constructor ; intros ; lra. Qed.
-
-#[export] Instance rmult_ac : ACOp Rmult.
-Proof. constructor ; intros ; lra. Qed.
-
-#[export] Instance r2_add_ac  : ACOp (@RealVectorSpace.add R2 _ _ _).
-Proof. 
-constructor.
-+ intros. now rewrite RealVectorSpace.add_comm.
-+ intros. now rewrite RealVectorSpace.add_assoc.
-Qed. *)
-
-(*Lemma master_key : unit. Proof. exact tt. Qed.
-Definition locked A := 
-  match master_key with 
-  | tt => fun x : A => x
-  end.
-
-Lemma lock : forall A x, x = locked x :> A.
-Proof. intros A x. unfold locked. case master_key. reflexivity. Qed.
-*)
-
-(* 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)
-  | 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 := 
-  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
-  | PNforall f => forall x, eval_pn l (f x)
-  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) 
-  | true, PNforall f => PNnot (PNforall f)
-  | false, PNnot a => push_neg_pn true a
-  | false, a => a
-  end.
++ cbv [fct_cte]. simpl. lra.
+Qed.  
 
-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.
-
-Inductive EnvEntry := 
-  | entry : (forall T : Type, T) -> EnvEntry.
-
-(* Turn a Prop into a PNProp. *)
-Ltac reify_aux term vars env := 
-  lazymatch term with 
-  | True => constr:((PNtrue, vars))
-  | False => constr:((PNfalse, vars))
-  | ~ ?t1 => 
-      match reify_aux t1 vars env with
-      | (?p1, ?vars') => constr:((PNnot p1, vars'))
-      end 
-  | ?t1 /\ ?t2 => 
-      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 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
+(* Simplify a goal of the form [derivable_pt_lim f x d], assuming 
+ * f is not a [fun x => ...], i.e. is something like [plus_fct (comp _ _) (fct_cte _)] *)
+Ltac simp_derivable_rec :=
+  match goal with 
+  | [ |- derivable_pt_lim Ranalysis1.id _ _ ] => apply derivable_pt_lim_id
+  | [ |- derivable_pt_lim (Ranalysis1.fct_cte _) _ _ ] => apply derivable_pt_lim_const
+  | [ |- derivable_pt_lim sqrt _ _ ] => apply derivable_pt_lim_sqrt ; simp_derivable_rec
+  | [ |- derivable_pt_lim (_ + _)%F _ _ ] => apply derivable_pt_lim_plus ; simp_derivable_rec
+  | [ |- derivable_pt_lim (_ * _)%F _ _ ] => apply derivable_pt_lim_mult ; simp_derivable_rec
+  | [ |- derivable_pt_lim (_ / _)%F _ _ ] => apply derivable_pt_lim_div ; simp_derivable_rec
+  | [ |- derivable_pt_lim (/ _)%F _ _ ] => apply derivable_pt_lim_inv ; simp_derivable_rec
+  | [ |- derivable_pt_lim (Ranalysis1.comp _ _)%F _ _ ] => apply derivable_pt_lim_comp ; simp_derivable_rec
+  | _ => idtac
   end.
 
-Ltac reify t := reify_aux t (@nil Prop) (@nil EnvEntry).
-
-Ltac push_negs := 
+(* Recursively break up a goal of the form [derivable_pt_lim f x d]. 
+ * To have any hope this works, you better use an existential variable for [d],
+ * i.e. use [evar (e : R). replace d with e. simp_derivable. unfold e.] and then prove e = d. *)
+Ltac simp_derivable :=
   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 List.nth]*)
-          end
-      end
+  | [ |- derivable_pt_lim ?f _ _ ] => 
+      let f_1 := eval cbv beta in (f Ranalysis_reg.AppVar) in 
+      let f_2 := Ranalysis_reg.rew_term f_1 in 
+      change f with f_2 ;
+      simp_derivable_rec
   end.
 
-
-Lemma test : forall x, x = S x.
-Proof. push_negs.*)
+(* Try to prove a goal of the form [derivable_pt_lim f x d], where [d] can be any expression. *)
+Ltac prove_derivable_pt_lim := 
+  lazymatch goal with 
+  | [ |- derivable_pt_lim _ _ ?l ] => 
+      let l_evar := fresh "l" in 
+      evar (l_evar : R) ;
+      replace l with l_evar ; 
+      [simp_derivable | unfold l_evar] ;
+      simp_fct
+  end.
\ No newline at end of file
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 064bc846505d7cf89b88d63523269b98c12b11f5..61d3f03c9b6237c7a5683cd47fea2dbfd4b2f9c5 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -854,27 +854,31 @@ case (x =?= w).
   - rewrite norm_defined. rewrite R2sub_origin. tauto.
 Qed.
 
+
 Lemma one_plus_sqrt_deriv (c : R) : 
   (-1 < c)%R -> derivable_pt_lim (fun x => sqrt (1 + x)%R) c (/ (2 * sqrt (1 + c)))%R.
 Proof. 
-intros Hc.
-assert (H : derivable_pt (fun x => sqrt (1 + x)) c). 
-{ reg. lra. }
-rewrite <-(derive_pt_eq _ _ _ H). reg. lra.
+intros Hc. prove_derivable_pt_lim.
++ lra.
++ lra.
 Qed.
 
 Lemma one_plus_sqrt_deriv_twice (c : R) : 
-  (-1 < c)%R -> derivable_pt_lim (fun x => (/ (2 * sqrt (1 + x)))%R) c (- / (8 * Rpower (1 + c) (3/2)))%R.
+  (-1 < c)%R -> derivable_pt_lim (fun x => (/ (2 * sqrt (1 + x)))%R) c (- / (4 * Rpower (1 + c) (3/2)))%R.
 Proof. 
-intros Hc.
-assert (H : derivable_pt (fun x => / (2 * sqrt (1 + x)))%R c). 
-{ reg.
-  + lra.
-  + intros H1. apply Rmult_integral in H1. destruct H1 as [H1 | H1] ; [lra |].
-    assert (H2 : (0 <= 1 + c)%R) by lra.
-    apply (sqrt_eq_0 _ H2) in H1. lra.
-}  
-Admitted.
+intros Hc. prove_derivable_pt_lim.
++ lra.
++ enough (0 < sqrt (1 + c))%R by lra.
+  apply sqrt_lt_R0. lra.
++ rewrite Rmult_0_l, Rplus_0_l, Rplus_0_l, Rmult_1_r.
+  rewrite Ropp_div. f_equal. 
+  unfold Rdiv, Rsqr. repeat rewrite Rinv_mult. repeat rewrite <-Rmult_assoc.
+  rewrite Rinv_r, Rmult_1_l by lra.
+  enough ((/ sqrt (1 + c) * / sqrt (1 + c) * / sqrt (1 + c))%R =
+    (/ Rpower (1 + c) (3 * / 2))%R) by lra.
+  repeat rewrite <-Rinv_mult. f_equal.
+  rewrite <-Rpower_sqrt by lra. repeat rewrite <-Rpower_plus. f_equal. lra.
+Qed.
 
 Lemma Rabs_le_iff (a b : R) : (-b <= a <= b)%R <-> (Rabs a <= b)%R.
 Proof. unfold Rabs. case (Rcase_abs a) ; lra. Qed.
@@ -885,12 +889,12 @@ Lemma sqrt_bound_helper (x : R) :
     exists y z, 
       Rabs y <= Rabs x /\
       Rabs z <= Rabs y /\
-      sqrt (1 + x) = 1 + x / 2 - x * y / (8 * Rpower (1 + z) (3/2)))%R.
+      sqrt (1 + x) = 1 + x / 2 - x * y / (4 * Rpower (1 + z) (3/2)))%R.
 Proof.
 intros Hx_abs. rewrite <-Rabs_le_iff in Hx_abs.
 remember (fun x => sqrt (1 + x)) as f.
 remember (fun x => / (2 * sqrt (1 + x)))%R as f'.
-remember (fun x => - / (8 * Rpower (1 + x) (3/2)))%R as f''.
+remember (fun x => - / (4 * Rpower (1 + x) (3/2)))%R as f''.
 case (Rtotal_order 0 x) as [Hx | [Hx | Hx]].
 + assert (Hmvt := MVT_cor2 f f' 0 x Hx). feed Hmvt.
   { intros y Hy. rewrite Heqf, Heqf'. apply one_plus_sqrt_deriv. lra. }
@@ -964,13 +968,13 @@ Lemma sqrt_bound :
       sqrt (1 + x) <= 1 + x / 2 + c * Rsqr x /\
       sqrt (1 + x) >= 1 + x / 2 - c * Rsqr x)%R.
 Proof.
-enough (H : exists c, (0 < c)%R /\ forall y, (Rabs y <= 1 / 2 -> Rabs (/ (8 * Rpower (1 + y) (3/2))) < c)%R).
+enough (H : exists c, (0 < c)%R /\ forall y, (Rabs y <= 1 / 2 -> Rabs (/ (4 * Rpower (1 + y) (3/2))) < c)%R).
 { 
   destruct H as [c [Hc H]]. exists c. split.
   + exact Hc. 
   + intros x Hx. 
     destruct (sqrt_bound_helper _ Hx) as [y [z [Hy [Hz Hsqrt]]]].
-    assert (Hbound : (Rabs (x * y / (8 * Rpower (1 + z) (3 / 2))) <= c * x²)%R).
+    assert (Hbound : (Rabs (x * y / (4 * Rpower (1 + z) (3 / 2))) <= c * x²)%R).
     { 
       unfold Rdiv. rewrite Rabs_mult, Rmult_comm. 
       apply Rmult_le_compat ; [pos_R | pos_R | | ].
@@ -981,19 +985,19 @@ enough (H : exists c, (0 < c)%R /\ forall y, (Rabs y <= 1 / 2 -> Rabs (/ (8 * Rp
 
     split.
     - rewrite Hsqrt. apply Rplus_le_compat_l.
-      transitivity (Rabs (- (x * y / (8 * Rpower (1 + z) (3 / 2)))))%R ; [apply Rle_abs |]. 
+      transitivity (Rabs (- (x * y / (4 * Rpower (1 + z) (3 / 2)))))%R ; [apply Rle_abs |]. 
       rewrite Rabs_Ropp. exact Hbound.
     - rewrite Hsqrt. apply Rle_ge, Rplus_le_compat_l, Ropp_le_contravar.
-      transitivity (Rabs (x * y / (8 * Rpower (1 + z) (3 / 2))))%R ; [apply Rle_abs |].
+      transitivity (Rabs (x * y / (4 * Rpower (1 + z) (3 / 2))))%R ; [apply Rle_abs |].
       exact Hbound.
 } 
 enough (H : exists c, (0 < c)%R /\ forall y, (Rabs y <= 1 / 2 -> Rpower (1 + y) (3/2) > c)%R).
 {
-  destruct H as [c [Hc H]]. exists (/ (8 * c))%R. 
+  destruct H as [c [Hc H]]. exists (/ (4 * c))%R. 
   split.
   + pos_R.
   + intros y Hy. specialize (H y Hy).
-    rewrite Rabs_inv, Rabs_mult, (Rabs_right 8) by lra.
+    rewrite Rabs_inv, Rabs_mult, (Rabs_right 4) by lra.
     apply Rinv_lt_contravar.
     - pos_R.
     - apply Rmult_lt_compat_l ; [lra |].
@@ -1631,13 +1635,12 @@ Proof. Admitted.
 Lemma weber_majority_weak ps w : 
   countA_occ equiv R2_EqDec w ps >= (Nat.div2 (length ps + 1)) -> Weber ps w.
 Proof.
-(* intros Hcount. rewrite ge_le_iff in Hcount. *)
+intros Hcount. rewrite ge_le_iff in Hcount. rewrite weber_first_order.
 (* rewrite weber_first_order. rewrite list_sumVS_norm. *)
 (* rewrite (@list_sum_le _ (alls 1%R (Nat.div2 (length ps + 1)))). *)
 (* + rewrite list_sum_alls, Rmult_1_r. apply le_INR. assumption. *)
 (* + etransitivity ; [|exact Hcount]. *)
-
- Admitted.
+Admitted.
 
 Lemma weber_majority ps w : 
   countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w.