Library gravityCenter

Require Import triangle_midpoints_theorems.
Require Export perp_bisect.

Section GravityCenter.

Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Context `{InterDec:InterDecidability Tpoint Col}.

Lemma intersection_two_medians_exist :
∀ A B C I J,
 ¬Col A B C →
 is_midpoint I B C → is_midpoint J A C →
 ∃ G, Col G A I ∧ Col G B J.
Proof with finish.
intros.
assert_bet.
elim (inner_pasch A B C J I)...
intro G;intros.
∃ G.
spliter;assert_cols;split...
Qed.

Lemma intersection_two_medians_exist_unique :
∀ A B C I J,
 ¬Col A B C →
 is_midpoint I B C → is_midpoint J A C →
 ∃! G, Col G A I ∧ Col G B J.
Proof with finish.
intros.
elim (intersection_two_medians_exist A B C I J H H0 H1); intros G HG; spliter.
∃ G.
unfold unique.
assert_all.
repeat split...
intros G' HG'; spliter.
apply inter_unicity with A I B J...
intro; search_contradiction.
show_distinct' B J...
Qed.

Definition is_gravity_center G A B C :=
 ¬ Col A B C ∧
 ∃ I, ∃ J, is_midpoint I B C ∧ is_midpoint J A C ∧ Col G A I ∧ Col G B J.

Lemma is_gravity_center_exist_unique : ∀ A B C,
  ¬ Col A B C →
  ∃! G, is_gravity_center G A B C.
Proof with finish.
intros.
assert_diffs.
Name I the midpoint of B and C.
Name J the midpoint of A and C.
elim (intersection_two_medians_exist A B C I J H H1 H4); intros G HG; spliter.
∃ G; unfold unique; unfold is_gravity_center; repeat split...
∃ I; ∃ J; do 3 (split; finish).
intros G' HG'; spliter; decompose [ex and] H8;clear H8.
assert_all.
apply inter_unicity with A x B x0...
intro;search_contradiction.
show_distinct' B x0...
Qed.

Ltac intersection_medians G A B C I J H1 H2 H3 :=
 let T := fresh in assert(T:= intersection_two_medians_exist A B C I J H1 H2 H3);
 ex_and T G.

Tactic Notation "Name" ident(G) "the" "intersection" "of" "the" "medians" "(" ident(A) ident(I) ")" "which" "is" "a" "median" "since" ident(H2) "and" "(" ident(B) ident(J) ")" "which" "is" "a" "median" "since" ident(H3) "of" "the" "non-flat" "triangle" ident(A) ident(B) ident(C) ident(H1) :=
 intersection_medians G A B C I J H1 H2 H3.

Lemma three_medians_intersect:
 ∀ A B C I J K,
 ¬Col A B C →
 is_midpoint I B C →
 is_midpoint J A C →
 is_midpoint K A B →
 ∃ G, Col G A I ∧ Col G B J ∧Col G C K.
Proof with assert_all.
intros.
assert_diffs.
Name G the intersection of the medians (A I)
     which is a median since H0 and (B J)
     which is a median since H1
     of the non-flat triangle A B C H.
∃ G; repeat split; try assumption.
Name D the symmetric of C wrt G.
assert_all.
show_distinct' A D.
permutation_intro_in_hyps.
assert (Par1 :=
     triangle_mid_par A D C G J H13 H14 H1).
show_distinct' B G.
assert (Par G B A D)
     by (perm_apply (par_col_par A D G J B)).
show_distinct' B D.
assert (Par2 :=
     triangle_mid_par B D C G I H103 H14 H0).
show_distinct' A G.
assert (Par G A D B)
     by (perm_apply (par_col_par B D G I A))...
show_distinct' D G.
assert (¬ Col G A D)
     by (intro; search_contradiction).
assert (Parallelogram G A D B)
     by (apply (par_2_plg G A D B); finish).
Name Z the intersection of the diagonals (G D)
     and (A B) of the parallelogram H17...
ColR.
Qed.

End GravityCenter.