Library midpoint_thales

Require Import triangle_midpoints_theorems.

Section T_42.

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

Lemma midpoint_thales : ∀ o a b c : Tpoint,
   ¬ Col a b c →
   is_midpoint o a b →
   Cong o a o c →
   Per a c b.
Proof.
intros.
Name x the midpoint of c and a.
assert (Par_strict o x b c)
 by perm_apply (triangle_mid_par_strict_cong_simp c b a o x).
assert(Per o x a)
 by (∃ c;split;finish).
assert_diffs.
assert_cols.
assert(Hid2 : Perp o x c a)
 by perm_apply (col_per_perp o x a c).
assert (Perp b c c a).
 apply (par_perp_perp o x b c c a);finish.
 apply par_strict_par;finish. apply perp_per_1;Perp.
Qed.

Lemma midpoint_thales_reci :
  ∀ a b c o: Tpoint,
   Per a c b →
   ¬Col a b c →
   is_midpoint o a b →
   Cong o a o b ∧ Cong o b o c.
Proof.
intros.

assert_diffs.

assert_congs.
split.
Cong.

assert(Hmid := midpoint_existence a c).
destruct Hmid.

assert(Hpar : Par c b x o).
apply (triangle_mid_par c b a o x);finish.


assert(Hper : Perp c b c a).
apply perp_left_comm.
apply per_perp.
auto.
auto.
Perp.

assert(HH := par_perp_perp c b x o c a Hpar Hper).
assert(Hper2 : Perp c x o x).
apply (perp_col c a o x x).
assert_diffs.
finish.
Perp.
assert_cols.
Col.

apply perp_left_comm in Hper2.
apply perp_perp_in in Hper2.
apply perp_in_comm in Hper2.
apply perp_in_per in Hper2.
apply l8_2 in Hper2.

unfold Per in Hper2.
destruct Hper2.
spliter.
apply l7_2 in H8.
assert(HmidU := l7_9 a x0 x c H2 H8).
rewrite <- HmidU in ×.
unfold is_midpoint in H2.
spliter.
apply cong_left_commutativity in H9.
apply cong_transitivity with (C:=o)(D:=a).
Cong.
Cong.
Qed.

End T_42.