proposition: Lemma thales_postulate__thales_converse_postulate : thales_postulate -> thales_converse_postulate.
proof: Proof. intros thales A B C M HM HPer. destruct (col_dec A B C) as [|HNCol]. destruct (l8_9 A C B); Col; subst; Cong. assert_diffs. assert(M <> C) by (intro; subst; apply HNCol; Col). destruct (segment_construction_3 M C M A) as [C' [HC' HCong]]; auto. apply cong_symmetry in HCong. elim(eq_dec_points C C'). intro; subst; assumption. intro. exfalso. assert_diffs. assert(~ Col A B C') by (intro; apply HNCol; ColR). assert(~ Col A C C') by (intro; apply HNCol; ColR). assert(~ Col B C C') by (intro; apply HNCol; ColR). assert_diffs. assert(CongA A C B A C' B). apply l11_16; auto; apply (thales _ _ _ M); assumption. assert(OS A B C C') by (apply (out_one_side_1 _ _ _ _ M); Col). destruct HC' as [_ [_ [HMCC'|HMC'C]]]. - assert(Hlta : LtA A C' B A C B); [|destruct Hlta; CongA]. apply os3__lta; Side; apply (one_side_transitivity _ _ _ M). apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply out_one_side; Col; apply l6_6; apply bet_out; Between. - assert(Hlta : LtA A C B A C' B); [|destruct Hlta; CongA]. apply os3__lta; Side; apply (one_side_transitivity _ _ _ M). apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply invert_one_side; apply out_one_side; Col; apply l6_6; apply bet_out; Between. apply out_one_side; Col; apply l6_6; apply bet_out; Between. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch11_angles