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

Section alternate_interior_angles_consecutive_interior_angles.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma alternate_interior__consecutive_interior :
   alternate_interior_angles_postulate -> consecutive_interior_angles_postulate.
Proof.
(* Goal: forall _ : @alternate_interior_angles_postulate Tn, @consecutive_interior_angles_postulate Tn *)
  intros aia A B C D Hos HPar.
(* Goal: @SuppA Tn A B C B C D *)
  split.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A B A') (@CongA Tn B C D C B A')) *)
    assert_diffs; auto.
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A B A') (@CongA Tn B C D C B A')) *)
  destruct (segment_construction A B B A) as [A' []].
(* Goal: @ex (@Tpoint Tn) (fun A' : @Tpoint Tn => and (@Bet Tn A B A') (@CongA Tn B C D C B A')) *)
  exists A'; split; trivial.
(* Goal: @CongA Tn B C D C B A' *)
  apply conga_comm, conga_sym, aia; [|assert_diffs; apply par_col_par_2 with A; Col; Par].
(* Goal: @TS Tn B C A' D *)
  apply l9_2, l9_8_2 with A; trivial.
(* Goal: @TS Tn B C A A' *)
  apply one_side_not_col123 in Hos.
(* Goal: @SuppA Tn A B C B C D *)
  repeat split.
(* Goal: not (@Col Tn A B C) *)
(* Goal: not (@Col Tn A' B C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B C) (@Bet Tn A T A')) *)
    Col.
(* Goal: not (@Col Tn A' B C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B C) (@Bet Tn A T A')) *)
    intro; apply Hos; ColR.
(* Goal: not (@Col Tn A B C) *)
(* Goal: not (@Col Tn A' B C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T B C) (@Bet Tn A T A')) *)
  exists B; split; Col.
Qed.

End alternate_interior_angles_consecutive_interior_angles.
