proposition: Lemma thales_converse_theorem : forall A B C M, Midpoint M A B -> Per A C B -> Cong M A M C.
proof: Proof. apply thales_postulate__thales_converse_postulate. unfold thales_postulate; apply thales_theorem. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec