diff --git a/CaseStudies/Gathering/InR2/Weber/Line.v b/CaseStudies/Gathering/InR2/Weber/Line.v
index db0f244b66876e4dea17961b2b13553e8448e5ef..07995dcd00e7127ad27a5a244a38e0983758eb4e 100644
--- a/CaseStudies/Gathering/InR2/Weber/Line.v
+++ b/CaseStudies/Gathering/InR2/Weber/Line.v
@@ -1046,21 +1046,6 @@ Lemma line_right_spec L x y ps :
InA equiv y (L^right x ps) <-> (InA equiv y ps /\ (L^P y > L^P x)%R).
Proof. unfold line_right. now rewrite filter_InA, Rltb_true ; [|intros ? ? ->]. Qed.
-Lemma line_left_diff L a ps:
- ((L ^left) a ps) <> nil ->
- aligned_on L ps ->
- (L ^-P) ((L ^max) ((L ^left) a ps)) <> a.
-Proof.
- intros h_left h_align.
- intro abs.
- assert (aligned_on L ((L ^left) a ps)) as h_align'.
- { eapply aligned_on_inclA with ps;auto.
- apply line_left_inclA. }
- specialize (line_iP_max_InA L _ h_left h_align') as h.
- rewrite abs in h.
- rewrite line_left_spec in h.
- lra.
-Qed.
Lemma line_left_on_right_partition L x ps :
PermutationA equiv ps (L^left x ps ++ L^on x ps ++ L^right x ps).
@@ -1155,6 +1140,52 @@ Proof.
lra.
Qed.
+Lemma line_left_diff L a ps:
+ ((L ^left) a ps) <> nil ->
+ aligned_on L ps ->
+ (L ^-P) ((L ^max) ((L ^left) a ps)) =/= a.
+Proof.
+ intros h_left h_align.
+ intro abs.
+ assert (aligned_on L ((L ^left) a ps)) as h_align'.
+ { eapply aligned_on_inclA with ps;auto.
+ apply line_left_inclA. }
+ specialize (line_iP_max_InA L _ h_left h_align') as h.
+ rewrite abs in h.
+ rewrite line_left_spec in h.
+ lra.
+Qed.
+
+
+Lemma eqlistA_nil_eq: forall [A : Type] (eqA : A -> A -> Prop) l, eqlistA eqA l nil <-> l = nil.
+Proof.
+ intros A eqA l.
+ split.
+ - induction l;intros;auto.
+ inversion H0.
+ - intro h.
+ subst.
+ apply eqlistA_nil.
+Qed.
+
+
+Lemma line_right_diff L a ps:
+ ((L ^right) a ps) <> nil ->
+ aligned_on L ps ->
+ (L ^-P) ((L ^min) ((L ^right) a ps)) =/= a.
+Proof.
+ intros h_right h_align.
+ rewrite <- line_reverse_iP_max.
+
+ rewrite <- line_reverse_left.
+ apply line_left_diff;auto.
+ - intro abs.
+ rewrite <- eqlistA_nil_eq with (eqA:=equiv) in abs .
+ rewrite line_reverse_left in abs.
+ rewrite eqlistA_nil_eq in abs.
+ contradiction.
+ - now apply -> aligned_on_reverse.
+Qed.
Lemma bipartition_min: forall L ps,
PermutationA equiv ps
@@ -1286,36 +1317,30 @@ Proof.
apply PermutationA_app_inv_l with (2:=h2).
typeclasses eauto.
Qed.
-(*
-Lemma aggravate_left': forall L ps w w',
- ((L^P w') < (L^P w))%R
- -> L^right w' (L^left w ps) = nil
- -> L^on w' ps = nil
- -> PermutationA equiv (L^left w ps) (L^left w' ps).
+
+
+Lemma aggravate_left' : forall L ps w w',
+ ((L ^P) w < (L ^P) w')%R ->
+ (L ^left) w' ((L ^right) w ps) = nil ->
+ (L ^on) w ps = nil ->
+ PermutationA equiv ((L ^left) w' ps) ((L ^left) w ps).
Proof.
- intros L ps w w' H0 H1 H2.
- specialize (line_left_on_right_partition L w' ps) as h1.
- specialize (line_left_on_right_partition L w ps) as h2.
- rewrite H2 in h1.
- rewrite app_nil_l in h1.
- assert (PermutationA equiv ((L ^right) w ps ++ (L ^on) w ps) ((L ^right) w' ps)).
- { specialize (line_left_on_right_partition L w ((L ^right) w' ps)) as h3.
- rewrite H2 in h3.
- rewrite app_nil_r in h3.
- rewrite <- aggravate_left in h3;auto.
- rewrite <- aggravate_on_left in h3;auto.
- rewrite h3.
- reflexivity.
- }
- rewrite <- H3 in h2.
- rewrite app_assoc in h1.
- rewrite h1 in h2 at 1.
- symmetry.
- apply PermutationA_app_inv_l with (2:=h2).
- typeclasses eauto.
+ intros L ps w w' H0 H1 H2.
+ remember (line_reverse L) as L'.
+
+ repeat rewrite <- line_reverse_right.
+ apply aggravate_right'.
+ - repeat rewrite line_reverse_proj.
+ lra.
+ - apply PermutationA_nil with equiv;auto.
+ + typeclasses eauto.
+ + setoid_rewrite line_reverse_left.
+ setoid_rewrite line_reverse_right.
+ now rewrite H1.
+ - apply eqlistA_nil_eq with equiv.
+ rewrite <- H2.
+ apply line_reverse_on.
Qed.
-*)
-
Lemma line_on_length_aligned L x ps :
aligned_on L (x :: ps) ->
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index a268413a98f2c3456ffe23544b0bc62d0e96423c..db7d8e5b79f134d938ed73502209cb218ff98977 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -2811,194 +2811,6 @@ Proof.
h_w_gt0 h_x_gt0 h_contains_m h_lt_wm h_lt_mx).
Qed.
-(*
-Lemma foo (x y m: R2): segment x y (middle x y) .
-Proof.
- remember (x::y::nil) as ps.
- remember (line_calc ps) as L.
- assert (ps <> nil) as h_nonnil.
- { now intro abs;subst. }
- assert (aligned ps) as h_align_ps.
- { unremember.
- apply aligned_spec.
- exists (y-x)%VS.
- intros p H.
- apply InA_singleton in H.
- rewrite H.
- exists 1%R.
- rewrite mul_1.
- symmetry.
- apply add_sub. }
- assert (line_contains L x) as h_line_x.
- { apply aligned_on_InA_contains with (ps:=ps);auto.
- + unremember.
- auto.
- + unremember.
- unremember in h_align_ps.
- apply line_calc_spec;auto. }
- assert (line_contains L y) as h_line_y.
- { apply aligned_on_InA_contains with (ps:=ps);auto.
- + unremember.
- auto.
- + unremember.
- unremember in h_align_ps.
- apply line_calc_spec;auto. }
-
- dup h_align_ps.
- rewrite (line_calc_spec ps) in h_align_ps'.
- reremember in h_align_ps'.
- specialize (line_iP_min_InA L ps h_nonnil h_align_ps') as h_min.
- specialize (line_iP_max_InA L ps h_nonnil h_align_ps') as h_max.
-
- apply (line_min_max_spec L (middle x y::ps)).
- { intro abs.
- discriminate. }
- 3:{ auto. }
- - admit.
- - red.
- specialize (line_middle L (middle x y :: ps)) as h_mid.
-
-
- assert (((L ^min) ps) = (L^P) x /\ (L ^max) ps = (L ^P) y \/ ((L ^min) ps) = ((L^P) y) /\ (L ^max) ps = (L ^P) x).
- { rewrite Heqps in h_min at 2.
- rewrite Heqps in h_max at 2.
- rewrite InA_cons in h_min,h_max.
- rewrite InA_cons in h_min,h_max.
- rewrite InA_nil in h_min,h_max.
-
- assert (InA equiv x ps) as h_in_x.
- { unremember; auto. }
- assert (InA equiv y ps) as h_in_y.
- { unremember; auto. }
-
- specialize (line_bounds L ps x h_in_x) as h_inx.
- specialize (line_bounds L ps y h_in_y) as h_iny.
-
- destruct h_min as [h_min | [h_min | abs]]; try contradiction;
- destruct h_max as [h_max | [h_max | abs]]; try contradiction.
- - assert ((L ^-P) ((L ^min) ps) = x) as h_min' by auto.
- assert ((L ^-P) ((L ^max) ps) = x) as h_max' by auto.
- rewrite <- h_max' in h_inx.
- rewrite line_P_iP_max in h_inx.
- assert ((L ^P) x = (L ^P) y).
- { subst x.
-
- lra. }
- left.
-
-.
-
- specialize (line_min_le_max L ps) as h_minmax.
- admit. }
- destruct H as [ [h_min_x h_max_y] | [h_min_y h_max_x]].
- - rewrite h_min_x,h_max_y in h_mid.
- red.
- exists (1/2)%R.
- split; try lra.
- assert ((1 - 1 / 2 = 1/2)%R).
- { lra. }
- rewrite H.
- transitivity (1 / 2 * (x + y))%VS.
- 2:{ apply mul_distr_add. }
- reflexivity.
- - rewrite h_min_y,h_max_x in h_mid.
- red.
- exists (1/2)%R.
- split; try lra.
- assert ((1 - 1 / 2 = 1/2)%R).
- { lra. }
- rewrite H.
- transitivity (1 / 2 * (x + y))%VS.
- 2:{ apply mul_distr_add. }
- reflexivity.
-
-
-
-
-Lemma foo (x y m: R2): segment x y (middle x y) .
-Proof.
- remember (x::y::nil) as ps.
- remember (line_calc ps) as L.
- assert (aligned ps).
- { unremember.
- apply aligned_spec.
- exists (y-x)%VS.
- intros p H.
- apply InA_singleton in H.
- rewrite H.
- exists 1%R.
- rewrite mul_1.
- symmetry.
- apply add_sub. }
- assert (line_contains L x).
- { apply aligned_on_InA_contains with (ps:=ps);auto.
- + unremember.
- auto.
- + unremember.
- unremember in H.
- apply line_calc_spec;auto. }
- assert (line_contains L y).
- { apply aligned_on_InA_contains with (ps:=ps);auto.
- + unremember.
- auto.
- + unremember.
- unremember in H.
- apply line_calc_spec;auto. }
- assert (line_contains L (middle x y)).
- { apply line_contains_middle;auto. }
-
- apply (segment_line L);auto.
- destruct (Rle_dec ((L ^P) x) ( (L ^P) y));[left|right].
- - split.
- + cbn.
- unremember.
- cbn.
- destruct (equiv_dec x y);cbn.
- * simpl.
- repeat rewrite Rmult_0_r.
- lra.
- * repeat rewrite Rmult_plus_distr_r.
- repeat rewrite Rmult_plus_distr_l.
- repeat rewrite Rmult_plus_distr_r.
- remember (fst x) as a.
- remember (fst y) as b.
- remember (snd x) as d.
- remember (snd y) as e.
- repeat rewrite Ropp_mult_distr_r_reverse.
- repeat rewrite Ropp_mult_distr_l_reverse.
- repeat rewrite Ropp_involutive.
- repeat rewrite Ropp_mult_distr_l_reverse.
- assert (a * b + - (a * a) + (- (a * b) + a * a) = 0)%R as h_simpl_1.
- { lra. }
- assert (d * e + - (d * d) + (- (d * e) + d * d) = 0)%R as h_simpl_2.
- { lra. }
- rewrite h_simpl_1, h_simpl_2.
- setoid_rewrite Rplus_comm at 8.
- setoid_rewrite Rplus_assoc at 3.
- setoid_rewrite Rplus_comm at 6.
- setoid_rewrite Rplus_assoc at 3.
- setoid_rewrite <- Rplus_assoc at 3.
- assert ((1 / 2 * a * b) + - (1 / 2 * b * a) = 0)%R as h_simpl_3 .
- { admit.
- }
- setoid_rewrite h_simpl_3.
-
- assert ((- (1 / 2 * a * a) + 1 / 2 * b * b) + (- (a * b) + a * a) == 1/2 * ((a + -b)* (a+ -b)))%R.
- { setoid_rewrite Rmult_plus_distr_r.
- repeat setoid_rewrite Rmult_plus_distr_l.
- (* setoid_rewrite Rmult_plus_distr_l. *)
- (* setoid_rewrite Rmult_plus_distr_r. *)
- admit. }
- admit.
- + admit.
- - admit.
-Admitted.
-
-Lemma bar (x y m: R2): x<>y -> strict_segment x y (middle x y) .
-Proof.
-
-Admitted.
-*)
(* When there are an odd number of points, the weber point is always unique. *)
Lemma weber_odd_unique ps w :
@@ -3335,25 +3147,890 @@ Proof.
apply (@weber_aligned L ps) ;auto. }
Qed.
-Lemma weber_segment_InA ps w1 w2 :
- (forall w, Weber ps w <-> segment w1 w2 w) ->
- InA equiv w1 ps /\ InA equiv w2 ps.
+Lemma Rabs_zero: forall r, Rabs r = 0%R -> r = 0%R.
Proof.
-(* Proof sketch: suppose w1 is not occupied, then there is a point
- close to w1 but outside the segment that is also a weber point
- (since left, right and on would be the same). This would be a
- contradiction. *)
+ intros r H.
+ destruct (equiv_dec r 0%R);auto.
+ exfalso.
+ assert (r <> 0%R) by auto.
+ apply Rabs_no_R0 in c.
+ contradiction.
+Qed.
+
+Lemma INR_zero n: INR n = 0%R <-> n = 0.
+Proof.
+ split.
+ - intros H.
+ destruct n;auto.
+ rewrite S_INR in H.
+ exfalso.
+ assert (0 <= INR n)%R.
+ { apply pos_INR. }
+ lra.
+ - intros H.
+ subst.
+ reflexivity.
+Qed.
+
+
+Lemma balance_conseq: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} (ps1 ps2 : list T),
+ (((^R ps1) - (^R ps2))%R = 0%R) ->
+ ps1 = nil -> ps2 = nil.
+Proof.
+ intros T S0 EQ0 VS ES ps1 ps2 h_balance_w H1.
+ subst.
+ cbn in h_balance_w.
+ rewrite Rminus_0_l in h_balance_w.
+ destruct (ps2);auto.
+ cbn [length] in h_balance_w.
+ apply Ropp_eq_0_compat in h_balance_w.
+ rewrite Ropp_involutive in h_balance_w.
+ apply INR_zero in h_balance_w.
+ discriminate.
+Qed.
+
+Lemma balance_conseq_2: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} (ps1 ps2 : list T),
+ (((^R ps1) - (^R ps2))%R = 0%R) ->
+ ps2 = nil -> ps1 = nil.
+Proof.
+ intros T S0 EQ0 VS ES ps1 ps2 h_balance_w H1.
+ subst.
+ cbn in h_balance_w.
+ rewrite Rminus_0_r in h_balance_w.
+ destruct (ps1);auto.
+ cbn [length] in h_balance_w.
+ apply INR_zero in h_balance_w.
+ discriminate.
+Qed.
+
+Lemma balance_nonnul_left: forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ (^R (L ^on) w ps) = 0%R ->
+ ((^R (L ^left) w ps) - (^R (L ^right) w ps))%R = 0%R ->
+ (L ^left) w ps <> nil.
+Proof.
+ intros L ps w h_nonnil h_unoccupied H1.
+ intro abs.
+ remember ((L ^left)w ps) as leftw in *.
+ remember ((L ^right)w ps) as rightw in *.
+ remember ((L ^on)w ps) as onw in *.
+ assert (rightw=nil).
+ { apply balance_conseq with leftw;auto. }
+ apply h_nonnil.
+ apply Preliminary.PermutationA_nil with (eqA:=eq);auto.
+ rewrite (line_left_on_right_partition L w ps).
+ reremember.
+ rewrite abs, H.
+ rewrite app_nil_l,app_nil_r.
+ apply INR_zero in h_unoccupied.
+ rewrite length_zero_iff_nil in h_unoccupied.
+ now rewrite h_unoccupied.
+Qed.
+
+Lemma balance_nonnul_right: forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ (^R (L ^on) w ps) = 0%R ->
+ ((^R (L ^left) w ps) - (^R (L ^right) w ps))%R = 0%R ->
+ (L ^right) w ps <> nil.
+Proof.
+ intros L ps w h_nonnil h_unoccupied H1.
+ specialize (balance_nonnul_left h_nonnil h_unoccupied H1) as h.
+ intro abs.
+ apply length_zero_iff_nil in abs.
+ apply (f_equal INR) in abs.
+ change (INR 0) with 0%R in abs.
+ apply h.
+ rewrite abs in H1.
+ apply length_zero_iff_nil.
+ apply INR_zero.
+ lra.
+Qed.
+
+Lemma weber_aligned_non_occupied:
+ forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ line_dir L =/= 0%VS ->
+ aligned_on L (w :: ps) ->
+ (^R (L ^on) w ps) = 0%R ->
+ Weber ps w ->
+ Weber ps ((L ^-P) ((L ^min) ((L ^right) w ps))). (* also treu for left *)
+Proof.
+ intros L ps w h_nonnil h_dir_nonnul h_align h_unoccupied h_weber_w.
+ assert (Rabs ((^R (L ^left) w ps) - (^R (L ^right) w ps)) = 0)%R as h_balance_w.
+ { specialize (@weber_aligned_spec_weak L ps w h_dir_nonnul h_align) as h.
+ apply h in h_weber_w.
+ specialize (Rabs_pos ((^R (L ^left) w ps) - (^R (L ^right) w ps))) as h'.
+ lra. }
+ apply Rabs_zero in h_balance_w.
+ remember ((L ^left)w ps) as leftw in *.
+ remember ((L ^right)w ps) as rightw in *.
+ remember ((L ^on)w ps) as onw in *.
+ remember ((L ^-P) ((L ^min) rightw)) as neighbor in *.
+
+ assert (leftw <> nil) as h_left_nonil.
+ { subst leftw.
+ apply balance_nonnul_left;subst;auto. }
+
+ assert (rightw <> nil) as h_right_nonil.
+ { subst.
+ apply balance_nonnul_right;auto. }
+
+ assert (aligned_on L ps) as h_align_ps.
+ { apply (aligned_on_cons_iff L w ps).
+ assumption. }
- intros h_forall.
+ assert (aligned_on L (neighbor :: ps)) as h_align_neigh.
+ { apply aligned_on_cons_iff;split;auto.
+ unremember. apply line_contains_proj_inv;auto. }
+
+ apply <- (@weber_aligned_spec_weak L);auto.
+ specialize (line_right_spec L w (L^-P((L ^min) ((L ^right) w ps))) ps) as hhh.
+ assert (((L ^P) w < (L ^P) neighbor)%R).
+ { subst.
+ apply hhh.
+ apply line_iP_min_InA;auto.
+ apply aligned_on_inclA with (ps':=ps);auto.
+ apply line_right_inclA. }
+
+ assert (PermutationA equiv ((L^left) (neighbor) ps) leftw) as h_perm_left_neigh.
+ { rewrite Heqleftw.
+ apply (aggravate_left' L ps w neighbor).
+ - assumption.
+ - reremember.
+ rewrite Heqneighbor.
+ apply line_left_iP_min.
+ - apply length_0.
+ apply INR_zero.
+ reremember.
+ lra. }
+
+ assert (PermutationA equiv ((L^right) w ps)
+ ((L^on) (neighbor) ps ++ (L^right) (neighbor) rightw)) as h_perm_right_neigh.
+ { assert ((L ^on) ((L ^-P) ((L ^min) rightw)) ps
+ = (L ^on) ((L ^-P) ((L ^min) rightw)) rightw)%R as heq_rightw.
+ { unremember.
+ apply aggravate_on_right;auto.
+ reremember.
+ assumption. }
+ subst neighbor.
+ rewrite heq_rightw at 1.
+ reremember.
+ apply bipartition_min. }
+ apply PermutationA_length in h_perm_right_neigh.
+ rewrite app_length in h_perm_right_neigh.
+ apply (f_equal INR) in h_perm_right_neigh.
+ rewrite plus_INR in h_perm_right_neigh.
+ assert ((^R (L ^on) neighbor ps) = (^R (L ^right) w ps) - (^R (L ^right) neighbor rightw))%R as h_balance' by lra.
+ rewrite h_balance'.
+ reremember in h_perm_right_neigh.
+ reremember.
+ assert (((^R leftw) = (^R rightw)))%R as h_balance_w' by lra.
+ reremember.
+ (* rewrite h_balance_w'. *)
+ apply Req_le.
+ assert ((^R (L ^right) neighbor ps)=(^R (L ^right) neighbor rightw))%R as h_same.
+ { unremember.
+ rewrite <- aggravate_right;auto.
+ rewrite line_P_iP;auto.
+ reremember.
+ specialize (line_right_spec L w ((L^-P) ((L ^min) rightw)) ps) as h_right.
+ assert (InA equiv ((L ^-P) ((L ^min) rightw)) ((L ^right) w ps)) as h_InA_minright.
+ { rewrite <- Heqrightw.
+ apply line_iP_min_InA;auto.
+ apply aligned_on_inclA with ps.
+ - unremember. apply line_right_inclA.
+ - apply (aligned_on_cons_iff L w ps);auto. }
+ rewrite h_right in h_InA_minright.
+ destruct h_InA_minright as [h_InA h_gt].
+ rewrite line_P_iP in h_gt;auto. }
+
+ rewrite Rabs_pos_eq.
+ - rewrite h_same.
+ rewrite h_perm_left_neigh.
+ rewrite h_balance_w'.
+ reflexivity.
+ - apply Rle_minus_sim.
+
+ reremember in h_balance'.
+ rewrite h_same.
+ rewrite h_perm_left_neigh.
+ rewrite h_balance_w'.
+ rewrite (line_left_on_right_partition L neighbor rightw) at 2.
+ assert ((^R (L ^left) neighbor rightw) >=0)%R.
+ { subst neighbor.
+ rewrite line_left_iP_min.
+ cbn.
+ lra. }
-Admitted.
+ assert ((^R (L ^on) neighbor rightw) >=0)%R.
+ { apply Rle_ge.
+ apply pos_INR. }
+ repeat rewrite app_length.
+ repeat rewrite plus_INR.
+ lra.
+Qed.
-(*
-Lemma weber_segment_InA' ps w1 w2 :
- (forall w, Weber ps w <-> segment w1 w2 w)
- <-> InA equiv w1 ps /\ InA equiv w2 ps /\ Weber ps w1 /\ Weber ps w2.
-Proof. Admitted.
-*)
-End WeberPoint.
+Lemma weber_aligned_non_occupied_2:
+ forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ line_dir L =/= 0%VS ->
+ aligned_on L (w :: ps) ->
+ (^R (L ^on) w ps) = 0%R ->
+ Weber ps w ->
+ Weber ps ((L ^-P) ((L ^max) ((L ^left) w ps))).
+Proof.
+ intros L' ps w h_nonnil h_dir_nonnul h_align h_unoccupied h_weber_w.
+ remember (line_reverse L') as L.
+ rewrite <- line_reverse_right.
+ rewrite <- line_reverse_iP_min.
+ reremember.
+ apply weber_aligned_non_occupied;auto.
+ - subst.
+ destruct L';cbn.
+ cbn in h_dir_nonnul.
+ intro abs.
+ apply h_dir_nonnul.
+ inversion abs.
+ destruct line_dir;cbn in *.
+ assert (r = 0%R) by lra.
+ assert (r0 = r%R) by lra.
+ rewrite H2,H.
+ reflexivity.
+ - subst.
+ rewrite <- aligned_on_reverse;auto.
+ - rewrite <- line_reverse_on in h_unoccupied.
+ subst.
+ assumption.
+Qed.
+
+Lemma weber_aligned_non_occupied_neighbor_l:
+ forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ line_dir L =/= 0%VS ->
+ aligned_on L (w :: ps) ->
+ (^R (L ^on) w ps) = 0%R ->
+ Weber ps w ->
+ forall x,
+ line_contains L x ->
+ PermutationA equiv (L^right x ps) (L^right w ps) ->
+ (^R (L ^on) x ps) = 0%R
+ -> Weber ps x.
+Proof.
+ intros L ps w h_nonnil h_dir_nonnul h_align h_unoccupied h_weber_w x h_line_contains_x h_neighbor h_on_0.
+ assert ( (^R (L ^on) w ps) = ^R (L ^on) x ps) as heq_on.
+ { now rewrite h_on_0, h_unoccupied. }
+ assert ( (^R (L ^left) w ps) = ^R (L ^left) x ps).
+ { specialize (line_left_on_right_partition L x ps) as h.
+ rewrite (line_left_on_right_partition L w ps) in h at 1.
+ apply PermutationA_length in h.
+ apply (f_equal INR) in h.
+ repeat rewrite app_length in h.
+ repeat rewrite plus_INR in h.
+ apply PermutationA_length in h_neighbor.
+ apply (f_equal INR) in h_neighbor.
+ lra. }
+ apply (@weber_aligned_spec_weak L);auto.
+ - apply aligned_on_cons_iff;split;auto.
+ apply aligned_on_cons_iff in h_align;apply h_align.
+ - rewrite <- H, h_neighbor, <-heq_on.
+ apply (@weber_aligned_spec_weak L);auto.
+Qed.
+
+Lemma weber_aligned_non_occupied_neighbor_r:
+ forall [L : line] [ps : list R2] [w : R2],
+ ps <> nil ->
+ line_dir L =/= 0%VS ->
+ aligned_on L (w :: ps) ->
+ (^R (L ^on) w ps) = 0%R ->
+ Weber ps w ->
+ forall x,
+ line_contains L x ->
+ PermutationA equiv (L^left x ps) (L^left w ps) ->
+ (^R (L ^on) x ps) = 0%R ->
+ Weber ps x.
+Proof.
+ intros L ps w h_nonnil h_dir_nonnul h_align h_unoccupied h_weber_w x h_line_contains_x h_neighbor h_on_0.
+ apply (@weber_aligned_non_occupied_neighbor_l (line_reverse L) ps w);auto.
+ - intro abs.
+ inversion abs.
+ apply Ropp_eq_0_compat in H0.
+ rewrite Ropp_involutive in H0.
+ apply Ropp_eq_compat in H1.
+ repeat rewrite Ropp_involutive in H1.
+ apply h_dir_nonnul.
+ cbn.
+ destruct L;cbn in *.
+ destruct line_dir;cbn in *.
+ now subst.
+ - now rewrite <- aligned_on_reverse.
+ - now rewrite line_reverse_on.
+ - now rewrite <- line_reverse_contains.
+ - repeat rewrite line_reverse_right.
+ apply h_neighbor.
+ - now rewrite line_reverse_on.
+Qed.
+
+
+
+Lemma symetric_left_outside_seg: forall L (w1 w2 w:R2),
+ line_dir L =/= 0%VS ->
+ ((L ^P) w1 < (L ^P) w2)%R ->
+ line_contains L w1 ->
+ line_contains L w2 ->
+ w = (w1 + w1 - w2)%VS ->
+ ~ segment w1 w2 w.
+Proof.
+ intros L w1 w2 w h_dir_nonnull h_lt_w1_w2 h_contain_w1 h_contain_w2 heqw.
+ intro abs.
+ (* segment means w is a unary linear combination of w1 and w2
+ which is contradictory with w = (w1 + w1 - w2)%VS. *)
+ red in abs.
+ destruct abs as [t [ht1 ht2]].
+ change equiv with (@eq R2) in ht2.
+ rewrite heqw in ht2.
+ assert ((t * w1 + (2 - t) * w1 + (1 - t) * w2 + (t - 2) * w2)
+ == ((t * w1 + (1 - t) * w2) + (2 - t) * w1 + (t - 2) * w2)
+ )%VS as heq_expr.
+ { setoid_rewrite <- add_assoc at 2.
+ setoid_rewrite <- add_comm at 3.
+ setoid_rewrite add_assoc at 1.
+ reflexivity. }
+ assert ((w1 + w1 - w2) = (t * w1 + ((2 - t) * w1)) + (1 - t) * w2 + (t - 2) * w2)%VS as heq_expr_mul.
+ { setoid_rewrite <- add_assoc at 2.
+ repeat rewrite add_morph.
+ setoid_rewrite Rplus_comm at 1.
+ setoid_rewrite Rplus_assoc at 1.
+ rewrite Rplus_opp_l.
+ rewrite Rplus_0_r.
+ setoid_rewrite <- Rplus_assoc.
+ setoid_rewrite Rplus_assoc at 2.
+ rewrite Rplus_opp_l.
+ rewrite Rplus_0_r.
+ unfold R2.
+ assert ((1 + - (2)) = -1)%R as hR by lra.
+ rewrite hR.
+ setoid_rewrite minus_morph.
+ rewrite mul_1.
+ setoid_rewrite <- (mul_1 w1) at 1 2.
+ rewrite add_morph.
+ assert (1+1 = 2)%R as hR1 by lra.
+ rewrite hR1;auto. }
+ change equiv with (@eq R2) in heq_expr.
+ rewrite heq_expr in heq_expr_mul.
+ rewrite <- ht2 in heq_expr_mul.
+ clear heq_expr.
+ assert (((2 - t) * w1 - (2 - t) * w2)%VS == 0%VS) as heq_exp_t.
+ { apply (R2plus_compat_eq_r (opp (w1 + w1 - w2)%VS)) in heq_expr_mul.
+ assert ((w1 + w1 - w2 - (w1 + w1 - w2))%VS == 0)%VS as h_eq_zero.
+ { apply R2sub_origin. reflexivity. }
+ setoid_rewrite h_eq_zero in heq_expr_mul.
+ rewrite add_comm in heq_expr_mul.
+ setoid_rewrite add_assoc at 1 in heq_expr_mul.
+ setoid_rewrite add_assoc at 1 in heq_expr_mul.
+ setoid_rewrite add_comm at 3 in heq_expr_mul.
+ setoid_rewrite h_eq_zero in heq_expr_mul.
+ rewrite add_origin_l in heq_expr_mul.
+ rewrite <- (opp_opp ((t - 2) * w2))%VS in heq_expr_mul.
+ rewrite <- minus_morph in heq_expr_mul.
+ rewrite Ropp_minus_distr in heq_expr_mul.
+ symmetry.
+ apply heq_expr_mul. }
+ assert (w1 = w2) as heq_w1_w2.
+ { rewrite R2sub_origin in heq_exp_t.
+ apply mul_reg_l in heq_exp_t;auto.
+ lra. }
+ rewrite heq_w1_w2 in h_lt_w1_w2.
+ apply Rlt_irrefl with (1:=h_lt_w1_w2).
+Qed.
+
+Lemma symetric_left: forall L (w1 w2 w:R2),
+ line_dir L =/= 0%VS ->
+ ((L ^P) w1 < (L ^P) w2)%R ->
+ line_contains L w1 ->
+ line_contains L w2 ->
+ w = (w1 + w1 - w2)%VS ->
+ ((L^P w) < L^P w1)%R.
+Proof.
+ intros L w1 w2 w h_dir_nonnull h_lt_w1_w2 h_contain_w1 h_contain_w2 heqw.
+ red in h_contain_w1.
+ red in h_contain_w2.
+ cbn in *.
+ remember (fst w1) as x1 in *.
+ remember (fst w2) as x2 in *.
+ remember (snd w1) as y1 in *.
+ remember (snd w2) as y2 in *.
+ remember (line_dir L) as d.
+ remember (line_org L) as o.
+ remember (fst o) as xo.
+ remember (snd o) as yo.
+ remember (fst d) as xd.
+ remember (snd d) as yd.
+ remember ((sqrt (xd * xd + yd * yd))²)%R as nrm.
+ subst w.
+ cbn in *.
+ subst w1 w2.
+ cbn in *.
+ lra.
+Qed.
+
+Lemma line_on_zero L ps (w:R2):
+ aligned_on L ps ->
+ line_contains L w ->
+ ~InA equiv w ps ->
+ (^R (L ^on) w ps) = 0%R.
+Proof.
+ intros h_align h_contain h_notInA.
+ apply INR_zero.
+ apply length_zero_iff_nil.
+ unfold line_on.
+
+ rewrite -> filter_nilA with (eqA := eq);auto; try typeclasses eauto.
+ intros x H.
+ apply eqb_false_iff.
+ intro abs.
+ assert ((L ^P) w = (L ^P) x) as h_eq by auto.
+ apply (f_equal (line_proj_inv L)) in h_eq.
+ rewrite line_contains_def in h_eq;auto.
+ rewrite line_contains_def in h_eq;auto.
+ apply h_notInA.
+ subst.
+ assumption.
+Qed.
+
+Lemma weber_segment_InA_left ps w1 w2 L :
+ ps <> nil ->
+ line_dir L =/= 0%VS ->
+ w1 =/= w2 ->
+ aligned_on L ps ->
+ line_contains L w1 ->
+ line_contains L w2 ->
+ Weber ps w1 ->
+ (L^P w1 < L^P w2)%R ->
+ ~ InA equiv w1 ps ->
+ (exists w, ~segment w1 w2 w /\ Weber ps w).
+Proof.
+ intros h_nonnil h_dir_nonnull h_neq h_align_ps h_contain_w1 h_contain_w2 h_weber_w1 h_lt_w1_w2 absInA.
+ destruct (eqlistA_dec equiv_dec ((L^left w1 ps)) nil) as [heql_left_nil | hneql_left_nil].
+ - inversion heql_left_nil as [heq_left_nil | ].
+ alias (w1 + w1 - w2)%VS as w before h_neq.
+ assert (((L ^P) w < (L ^P) w1)%R) as hlt_proj.
+ { apply symetric_left with (w2 := w2);auto. }
+ exists w.
+ { split.
+ - apply symetric_left_outside_seg with (w1:=w1)(w2:=w2)(w:=w)(L:=L);auto.
+ - apply (@weber_aligned_non_occupied_neighbor_l L ps w1);auto.
+ + apply aligned_on_cons_iff;auto.
+ + apply line_on_zero;auto.
+ + subst w.
+ assert (w1 + (-1)%R * (w2 - w1) = (w1 + w1 - w2))%VS as heq.
+ { setoid_rewrite minus_morph.
+ setoid_rewrite <- mul_opp.
+ rewrite mul_1.
+ rewrite R2_opp_dist.
+ rewrite opp_opp.
+ setoid_rewrite add_comm at 2.
+ rewrite add_assoc.
+ reflexivity. }
+ rewrite <- heq.
+ apply line_contains_combine;auto.
+ + rewrite (aggravate_right' L ps w1 w); try lra.
+ * reflexivity.
+ * rewrite <- heq_left_nil.
+ reflexivity.
+ * apply length_zero_iff_nil.
+ apply INR_zero.
+ apply line_on_zero;auto.
+ + specialize (left_lt L ps w w1 hlt_proj) as h.
+ rewrite <- heq_left_nil in h.
+ cbn [length INR] in h.
+ assert (0 <= (^R (L ^left) w ps))%R.
+ { apply pos_INR. }
+ assert (0 <= (^R (L ^on) w ps))%R.
+ { apply pos_INR. }
+ lra. }
+ - assert (((L ^left) w1 ps) <> nil) as hneq_left_nil.
+ { rewrite <- eqlistA_Leibniz.
+ assumption. }
+ clear hneql_left_nil.
+ alias (L^-P (L^max (L^left w1 ps))) as w after h_nonnil.
+ specialize (line_left_diff L w1 ps hneq_left_nil h_align_ps) as h.
+ specialize (line_contains_proj_inv L ((L ^max) ((L ^left) w1 ps)) h_dir_nonnull) as h'.
+ reremember in h'.
+ exists w;split.
+ + intro abs.
+ rewrite -> (segment_line L) in abs;auto.
+ destruct abs as [[hle_w1_w hle_w_w2] | [hle_w2_w hle_w_w1] ].
+ 2:{ exfalso;lra. }
+ specialize (line_left_spec L w1 w ps) as h''.
+ assert (((L ^P) w < (L ^P) w1)%R).
+ { clear hle_w1_w hle_w_w2.
+ apply -> h''.
+ unremember.
+ apply line_iP_max_InA;auto.
+ apply aligned_on_inclA with (ps':=ps);auto.
+ apply line_left_inclA. }
+ exfalso.
+ lra.
+ + subst w.
+ apply weber_aligned_non_occupied_2;auto.
+ * apply aligned_on_cons_iff;auto.
+ * apply line_on_zero;auto.
+Qed.
+
+
+Lemma weber_segment_InA_1 ps w1 w2 L:
+ ps <> nil ->
+ w1 =/= w2 ->
+ aligned_on L ps ->
+ (L^P w1 < L^P w2)%R ->
+ (forall w, Weber ps w <-> segment w1 w2 w) ->
+ InA equiv w1 ps.
+Proof.
+(* Proof sketch: suppose w1 is not occupied, then there is a point
+ close to w1 but outside the segment that is also a weber point
+ (since left, right and on would be the same). This would be a
+ contradiction. *)
+
+ intros h_nonnil h_neq h_align h_lt_w1_w2 h_forall.
+
+ (* Frmo now on ps is supposed aligned. And w1 and w2 are also akigned with it. And they are weber points. *)
+ assert (Weber ps w1) as h_weber_w1.
+ { apply h_forall.
+ apply segment_start. }
+ assert (Weber ps w2) as h_weber_w2.
+ { apply h_forall.
+ apply segment_end. }
+ assert (line_contains L w1) as h_contain_w1.
+ { apply weber_aligned with ps;auto. }
+ assert (line_contains L w2) as h_contain_w2.
+ { apply weber_aligned with ps;auto. }
+ assert (line_dir L =/= 0%VS) as h_dir_nonnull.
+ { apply line_dir_nonnul with w1 w2;auto. }
+
+ apply decidable_not_not_iff.
+ { unfold Decidable.decidable.
+ destruct (InA_dec equiv_dec w1 ps);auto. }
+ intro absInA.
+ exfalso.
+ specialize (@weber_segment_InA_left ps w1 w2 L) as [w [hw1 hw2]];auto.
+ apply h_forall in hw2.
+ contradiction.
+Qed.
+
+Lemma weber_segment_InA_2 ps w1 w2 L:
+ ps <> nil ->
+ w1 =/= w2 ->
+ aligned_on L ps ->
+ (L^P w1 < L^P w2)%R ->
+ (forall w, Weber ps w <-> segment w1 w2 w) ->
+ InA equiv w2 ps.
+Proof.
+ intros h_nonnil h_neq HeqL h_lt_w1_w2 h_forall.
+ remember (line_reverse L) as L'.
+ apply (@weber_segment_InA_1 ps w2 w1 L').
+ - assumption.
+ - now symmetry.
+ - subst.
+ now rewrite <- aligned_on_reverse.
+ - subst.
+ repeat rewrite line_reverse_proj.
+ lra.
+ - now setoid_rewrite segment_sym.
+Qed.
+
+
+
+Lemma weber_segment_InA_3 ps w1 w2 L:
+ ps <> nil ->
+ w1 =/= w2 ->
+ aligned_on L ps ->
+ (L^P w2 < L^P w1)%R ->
+ (forall w, Weber ps w <-> segment w1 w2 w) ->
+ InA equiv w2 ps.
+Proof.
+ intros h_nonnil h_neq HeqL h_lt_w1_w2 h_forall.
+ apply (@weber_segment_InA_1 ps w2 w1 L).
+ - assumption.
+ - now symmetry.
+ - assumption.
+ - lra.
+ - now setoid_rewrite segment_sym.
+Qed.
+
+
+Lemma weber_segment_InA_4 ps w1 w2 L:
+ ps <> nil ->
+ w1 =/= w2 ->
+ aligned_on L ps ->
+ (L^P w2 < L^P w1)%R ->
+ (forall w, Weber ps w <-> segment w1 w2 w) ->
+ InA equiv w1 ps.
+Proof.
+ intros h_nonnil h_neq HeqL h_lt_w1_w2 h_forall.
+ remember (line_reverse L) as L'.
+ apply (@weber_segment_InA_1 ps w1 w2 L').
+ - assumption.
+ - now symmetry.
+ - subst.
+ now rewrite <- aligned_on_reverse.
+ - subst.
+ repeat rewrite line_reverse_proj.
+ lra.
+ - assumption.
+Qed.
+
+
+
+Lemma weber_segment_InA ps w1 w2 :
+ ps <> nil ->
+ w1 =/= w2 ->
+ (forall w, Weber ps w <-> segment w1 w2 w) ->
+ InA equiv w1 ps /\ InA equiv w2 ps.
+Proof.
+ intros h_nonnil h_neq h_forall.
+ remember (line_calc ps) as L.
+ destruct (aligned_on_dec L ps) as [h_align_ps | h_nalign_ps].
+ all:swap 1 2.
+ { (* If ps is not aligned, w1 and w2 can't be different *)
+ unremember in h_nalign_ps.
+ exfalso.
+ apply h_neq.
+ dup h_nalign_ps.
+ rewrite <- line_calc_spec in h_nalign_ps'.
+ specialize (@weber_Naligned_unique _ w1 h_nalign_ps') as h1.
+ specialize (@weber_Naligned_unique _ w2 h_nalign_ps') as h2.
+ rewrite h_forall in h1,h2.
+ specialize (h1 (segment_start w1 w2)) as [h11 h12].
+ specialize (h2 (segment_end w1 w2)) as [h21 h22].
+ { auto. } }
+ assert (Weber ps w1) as h_weber_w1.
+ { apply h_forall.
+ apply segment_start. }
+ assert (Weber ps w2) as h_weber_w2.
+ { apply h_forall.
+ apply segment_end. }
+ assert (line_contains L w1) as h_contain_w1.
+ { apply weber_aligned with ps;auto. }
+ assert (line_contains L w2) as h_contain_w2.
+ { apply weber_aligned with ps;auto. }
+ assert (line_dir L =/= 0%VS) as h_dir_nonnull.
+ { apply line_dir_nonnul with w1 w2;auto. }
+
+ destruct (Rlt_le_dec (L^P w1) (L^P w2)) as [h_lt_w1_w2|h_le_w2_w1].
+ { split.
+ - apply weber_segment_InA_1 with (w2:=w2)(L:=L);auto.
+ - apply weber_segment_InA_2 with (w1:=w1)(L:=L);auto. }
+ destruct (Rle_lt_or_eq_dec _ _ h_le_w2_w1) as [h_lt_w2_w1|h_eq_w2_w1].
+ { split.
+ - apply weber_segment_InA_4 with (w2:=w2)(L:=L);auto.
+ - apply weber_segment_InA_3 with (w1:=w1)(L:=L);auto. }
+ exfalso.
+ apply h_neq.
+ rewrite <- h_contain_w1.
+ rewrite <- h_contain_w2.
+ rewrite h_eq_w2_w1.
+ reflexivity.
+Qed.
+
+(*
+Lemma weber_segment_InA' ps w1 w2 :
+ (forall w, Weber ps w <-> segment w1 w2 w)
+ <-> InA equiv w1 ps /\ InA equiv w2 ps /\ Weber ps w1 /\ Weber ps w2.
+Proof. Admitted.
+*)
+
+End WeberPoint.
+
+
+
+
+(*
+Lemma foo (x y m: R2): segment x y (middle x y) .
+Proof.
+ remember (x::y::nil) as ps.
+ remember (line_calc ps) as L.
+ assert (ps <> nil) as h_nonnil.
+ { now intro abs;subst. }
+ assert (aligned ps) as h_align_ps.
+ { unremember.
+ apply aligned_spec.
+ exists (y-x)%VS.
+ intros p H.
+ apply InA_singleton in H.
+ rewrite H.
+ exists 1%R.
+ rewrite mul_1.
+ symmetry.
+ apply add_sub. }
+ assert (line_contains L x) as h_line_x.
+ { apply aligned_on_InA_contains with (ps:=ps);auto.
+ + unremember.
+ auto.
+ + unremember.
+ unremember in h_align_ps.
+ apply line_calc_spec;auto. }
+ assert (line_contains L y) as h_line_y.
+ { apply aligned_on_InA_contains with (ps:=ps);auto.
+ + unremember.
+ auto.
+ + unremember.
+ unremember in h_align_ps.
+ apply line_calc_spec;auto. }
+
+ dup h_align_ps.
+ rewrite (line_calc_spec ps) in h_align_ps'.
+ reremember in h_align_ps'.
+ specialize (line_iP_min_InA L ps h_nonnil h_align_ps') as h_min.
+ specialize (line_iP_max_InA L ps h_nonnil h_align_ps') as h_max.
+
+ apply (line_min_max_spec L (middle x y::ps)).
+ { intro abs.
+ discriminate. }
+ 3:{ auto. }
+ - admit.
+ - red.
+ specialize (line_middle L (middle x y :: ps)) as h_mid.
+
+
+ assert (((L ^min) ps) = (L^P) x /\ (L ^max) ps = (L ^P) y \/ ((L ^min) ps) = ((L^P) y) /\ (L ^max) ps = (L ^P) x).
+ { rewrite Heqps in h_min at 2.
+ rewrite Heqps in h_max at 2.
+ rewrite InA_cons in h_min,h_max.
+ rewrite InA_cons in h_min,h_max.
+ rewrite InA_nil in h_min,h_max.
+
+ assert (InA equiv x ps) as h_in_x.
+ { unremember; auto. }
+ assert (InA equiv y ps) as h_in_y.
+ { unremember; auto. }
+
+ specialize (line_bounds L ps x h_in_x) as h_inx.
+ specialize (line_bounds L ps y h_in_y) as h_iny.
+
+ destruct h_min as [h_min | [h_min | abs]]; try contradiction;
+ destruct h_max as [h_max | [h_max | abs]]; try contradiction.
+ - assert ((L ^-P) ((L ^min) ps) = x) as h_min' by auto.
+ assert ((L ^-P) ((L ^max) ps) = x) as h_max' by auto.
+ rewrite <- h_max' in h_inx.
+ rewrite line_P_iP_max in h_inx.
+ assert ((L ^P) x = (L ^P) y).
+ { subst x.
+
+ lra. }
+ left.
+
+.
+
+ specialize (line_min_le_max L ps) as h_minmax.
+ admit. }
+ destruct H as [ [h_min_x h_max_y] | [h_min_y h_max_x]].
+ - rewrite h_min_x,h_max_y in h_mid.
+ red.
+ exists (1/2)%R.
+ split; try lra.
+ assert ((1 - 1 / 2 = 1/2)%R).
+ { lra. }
+ rewrite H.
+ transitivity (1 / 2 * (x + y))%VS.
+ 2:{ apply mul_distr_add. }
+ reflexivity.
+ - rewrite h_min_y,h_max_x in h_mid.
+ red.
+ exists (1/2)%R.
+ split; try lra.
+ assert ((1 - 1 / 2 = 1/2)%R).
+ { lra. }
+ rewrite H.
+ transitivity (1 / 2 * (x + y))%VS.
+ 2:{ apply mul_distr_add. }
+ reflexivity.
+
+
+
+
+Lemma foo (x y m: R2): segment x y (middle x y) .
+Proof.
+ remember (x::y::nil) as ps.
+ remember (line_calc ps) as L.
+ assert (aligned ps).
+ { unremember.
+ apply aligned_spec.
+ exists (y-x)%VS.
+ intros p H.
+ apply InA_singleton in H.
+ rewrite H.
+ exists 1%R.
+ rewrite mul_1.
+ symmetry.
+ apply add_sub. }
+ assert (line_contains L x).
+ { apply aligned_on_InA_contains with (ps:=ps);auto.
+ + unremember.
+ auto.
+ + unremember.
+ unremember in H.
+ apply line_calc_spec;auto. }
+ assert (line_contains L y).
+ { apply aligned_on_InA_contains with (ps:=ps);auto.
+ + unremember.
+ auto.
+ + unremember.
+ unremember in H.
+ apply line_calc_spec;auto. }
+ assert (line_contains L (middle x y)).
+ { apply line_contains_middle;auto. }
+
+ apply (segment_line L);auto.
+ destruct (Rle_dec ((L ^P) x) ( (L ^P) y));[left|right].
+ - split.
+ + cbn.
+ unremember.
+ cbn.
+ destruct (equiv_dec x y);cbn.
+ * simpl.
+ repeat rewrite Rmult_0_r.
+ lra.
+ * repeat rewrite Rmult_plus_distr_r.
+ repeat rewrite Rmult_plus_distr_l.
+ repeat rewrite Rmult_plus_distr_r.
+ remember (fst x) as a.
+ remember (fst y) as b.
+ remember (snd x) as d.
+ remember (snd y) as e.
+ repeat rewrite Ropp_mult_distr_r_reverse.
+ repeat rewrite Ropp_mult_distr_l_reverse.
+ repeat rewrite Ropp_involutive.
+ repeat rewrite Ropp_mult_distr_l_reverse.
+ assert (a * b + - (a * a) + (- (a * b) + a * a) = 0)%R as h_simpl_1.
+ { lra. }
+ assert (d * e + - (d * d) + (- (d * e) + d * d) = 0)%R as h_simpl_2.
+ { lra. }
+ rewrite h_simpl_1, h_simpl_2.
+ setoid_rewrite Rplus_comm at 8.
+ setoid_rewrite Rplus_assoc at 3.
+ setoid_rewrite Rplus_comm at 6.
+ setoid_rewrite Rplus_assoc at 3.
+ setoid_rewrite <- Rplus_assoc at 3.
+ assert ((1 / 2 * a * b) + - (1 / 2 * b * a) = 0)%R as h_simpl_3 .
+ { admit.
+ }
+ setoid_rewrite h_simpl_3.
+
+ assert ((- (1 / 2 * a * a) + 1 / 2 * b * b) + (- (a * b) + a * a) == 1/2 * ((a + -b)* (a+ -b)))%R.
+ { setoid_rewrite Rmult_plus_distr_r.
+ repeat setoid_rewrite Rmult_plus_distr_l.
+ (* setoid_rewrite Rmult_plus_distr_l. *)
+ (* setoid_rewrite Rmult_plus_distr_r. *)
+ admit. }
+ admit.
+ + admit.
+ - admit.
+Admitted.
+
+Lemma bar (x y m: R2): x<>y -> strict_segment x y (middle x y) .
+Proof.
+
+Admitted.
+*)