proposition: Lemma thales_converse_theorem_1 : forall A B C O, A <> C -> B <> C -> Per A C B -> Cong O A O B -> Cong O A O C -> Coplanar A B C O -> Midpoint O A B.
proof: Proof. intros A B C O HAC HBC HPer HCong1 HCong2 HCop. destruct (midpoint_existence A B) as [M HM]. assert (M = O); [|subst; apply HM]. suma.assert_diffs. apply (cong4_cop2__eq A C B); Cong; [|Cop..]. apply cong_commutativity, thales_converse_theorem with B; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec