proposition: Lemma midpoint_thales_reci : forall a b c o: Tpoint, Per a c b -> Midpoint o a b -> Cong o a o b /\ Cong o b o c.
proof: Proof. intros. induction (col_dec a b c). induction (l8_9 a c b H); treat_equalities;assert_congs_perm;try split;finish. assert_diffs. assert_congs_perm. 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) by (apply perp_left_comm;apply per_perp;Perp). assert(Hcop : Coplanar x o c a) by Cop. assert(HH := cop_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. Col. assert_diffs. assert (Per o x c) by (apply perp_per_2;Perp). unfold Per in H8. destruct H8. spliter. apply l7_2 in H8. assert(HmidU := l7_9 a x0 x c H2 H8). subst. unfold Midpoint in H2. spliter. eCong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems