Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.

Section thales_converse_postulate_thales_existence.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma thales_converse_postulate__thales_existence : thales_converse_postulate -> existential_thales_postulate.
Proof.
(* Goal: forall _ : @thales_converse_postulate Tn, @existential_thales_postulate Tn *)
  intro thales.
(* Goal: @existential_thales_postulate Tn *)
  destruct lower_dim_ex as [C [A [B0]]].
(* Goal: @existential_thales_postulate Tn *)
  assert(HNCol : ~ Col C A B0) by (unfold Col; assumption).
(* Goal: @existential_thales_postulate Tn *)
  destruct (l10_15 C A C B0) as [B []]; Col.
(* Goal: @existential_thales_postulate Tn *)
  assert(~ Col C A B) by (apply (one_side_not_col123 _ _ _ B0); Side).
(* Goal: @existential_thales_postulate Tn *)
  assert(Per A C B) by Perp.
(* Goal: @existential_thales_postulate Tn *)
  destruct (midpoint_existence A B) as [M].
(* Goal: @existential_thales_postulate Tn *)
  exists A; exists B; exists C; exists M.
(* Goal: and (not (@Col Tn A B C)) (and (@Midpoint Tn M A B) (and (@Cong Tn M A M C) (@Per Tn A C B))) *)
  repeat (split; Col).
(* Goal: @Cong Tn M A M C *)
  apply (thales _ B); Col.
Qed.

End thales_converse_postulate_thales_existence.