Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch13_1.

Section playfair_midpoints.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma playfair_s_postulate_implies_midpoint_converse_postulate :
  playfair_s_postulate ->
  midpoint_converse_postulate.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, @midpoint_converse_postulate Tn *)
intros HP A; intros.
(* Goal: @Midpoint Tn Q A C *)
destruct (midpoint_existence A C) as [X HAC].
(* Goal: @Midpoint Tn Q A C *)
assert (X = Q).
(* Goal: @eq (@Tpoint Tn) X Q *)
(* Goal: @Midpoint Tn Q A C *)
 assert (Par_strict A B X P).
(* Goal: @Par_strict Tn A B X P *)
(* Goal: @eq (@Tpoint Tn) X Q *)
(* Goal: @Midpoint Tn Q A C *)
  apply triangle_mid_par with C; assumption.
(* Goal: @eq (@Tpoint Tn) X Q *)
(* Goal: @Midpoint Tn Q A C *)
 assert_diffs.
(* Goal: @eq (@Tpoint Tn) X Q *)
(* Goal: @Midpoint Tn Q A C *)
 assert_cols.
(* Goal: @eq (@Tpoint Tn) X Q *)
(* Goal: @Midpoint Tn Q A C *)
 apply l6_21 with A C P Q.
(* Goal: not (@Col Tn A C P) *)
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @Col Tn A C X *)
(* Goal: @Col Tn A C Q *)
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  intro.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @Col Tn A C X *)
(* Goal: @Col Tn A C Q *)
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  assert (Col A B C) by ColR.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @Col Tn A C X *)
(* Goal: @Col Tn A C Q *)
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  contradiction.
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @Col Tn A C X *)
(* Goal: @Col Tn A C Q *)
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  assert (Par A B Q P /\ A <> B /\ Q <> P) by (apply par_distincts; finish).
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
(* Goal: @Col Tn A C X *)
(* Goal: @Col Tn A C Q *)
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  spliter; intuition.
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  Col.
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  Col.
(* Goal: @Col Tn P Q X *)
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  destruct (HP A B Q P X P P) as [HCol1 HCol2]; Col; apply par_strict_par; Par.
(* Goal: @Col Tn P Q Q *)
(* Goal: @Midpoint Tn Q A C *)
  Col.
(* Goal: @Midpoint Tn Q A C *)
treat_equalities; assumption.
Qed.

End playfair_midpoints.