Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section playfair_alternate_interior_angles.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma playfair__alternate_interior :  playfair_s_postulate -> alternate_interior_angles_postulate.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, @alternate_interior_angles_postulate Tn *)
intros playfair A B C D Hts HPar.
(* Goal: @CongA Tn B A C D C A *)
assert(~ Col B A C) by (destruct Hts; auto).
(* Goal: @CongA Tn B A C D C A *)
assert(HD' := ex_conga_ts B A C A C B).
(* Goal: @CongA Tn B A C D C A *)
destruct HD' as [D' []]; Col.
(* Goal: @CongA Tn B A C D C A *)
apply (conga_trans _ _ _ D' C A).
(* Goal: @CongA Tn B A C D' C A *)
(* Goal: @CongA Tn D' C A D C A *)
CongA.
(* Goal: @CongA Tn D' C A D C A *)
assert_diffs.
(* Goal: @CongA Tn B A C D' C A *)
(* Goal: @CongA Tn D' C A D C A *)
apply (out_conga D C A D C A); try (apply out_trivial); CongA.
(* Goal: @Out Tn C D D' *)
apply (col_one_side_out _ A).
(* Goal: @Col Tn C D D' *)
(* Goal: @OS Tn C A D D' *)
assert (HP := playfair A B C D C D' C).
(* Goal: @Col Tn C D D' *)
(* Goal: @OS Tn C A D D' *)
destruct HP; Col.
(* Goal: @Par Tn A B C D' *)
(* Goal: @OS Tn C A D D' *)
apply l12_21_b; CongA; Side.
(* Goal: @OS Tn C A D D' *)
apply invert_one_side; exists B; split; Side.
Qed.

End playfair_alternate_interior_angles.