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

Section consecutive_interior_angles_alternate_interior_angles.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma consecutive_interior__alternate_interior :
   consecutive_interior_angles_postulate -> alternate_interior_angles_postulate.
Proof.
(* Goal: forall _ : @consecutive_interior_angles_postulate Tn, @alternate_interior_angles_postulate Tn *)
  intros cia A B C D Hts HPar.
(* Goal: @CongA Tn B A C D C A *)
  destruct (segment_construction D C C D) as [D' []].
(* Goal: @CongA Tn B A C D C A *)
  apply suppa2__conga123 with A C D'.
  - apply cia; [|assert_diffs; apply par_left_comm, par_col_par with D; Col].
(* Goal: @OS Tn A C B D' *)
    exists D; split; trivial.
(* Goal: @TS Tn A C D' D *)
    destruct Hts as [_ [HNCol _]].
(* Goal: @TS Tn A C D' D *)
    repeat split.
(* Goal: not (@Col Tn D' A C) *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn D' T D)) *)
      intro; apply HNCol; ColR.
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn D' T D)) *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn D' T D)) *)
    exists C; split; [Col|Between].
  - assert_diffs; split; auto.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn D C A') (@CongA Tn A C D' A C A')) *)
    exists D'; split; CongA.
Qed.

End consecutive_interior_angles_alternate_interior_angles.