proposition: Lemma midpoint_thales : forall O A B C : Tpoint, ~ Col A B C -> Midpoint O A B -> Cong O A O C -> Per A C B.
proof: 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 (exists 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 (cop_par_perp__perp O X B C C A);finish. apply perp_per_1;Perp. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems