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

Section alternate_interior_angles_playfair_bis.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma alternate_interior__playfair_aux : alternate_interior_angles_postulate ->
   forall A1 A2 B1 B2 C1 C2 P,
   Perp2 A1 A2 B1 B2 P -> ~ Col A1 A2 P -> Col P B1 B2 -> Coplanar A1 A2 B1 B2 ->
   Par A1 A2 C1 C2 -> Col P C1 C2 ->
   Col C1 B1 B2. (** "half" of playfair_bis *)
Proof.
(* Goal: forall (_ : @alternate_interior_angles_postulate Tn) (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : @Perp2 Tn A1 A2 B1 B2 P) (_ : not (@Col Tn A1 A2 P)) (_ : @Col Tn P B1 B2) (_ : @Coplanar Tn A1 A2 B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), @Col Tn C1 B1 B2 *)
  intros aip A1 A2 B1 B2 C1 C2 P HPerp2 HNC1 HPB HCop HParAC HPC.
(* Goal: @Col Tn C1 B1 B2 *)
  elim(eq_dec_points P C1).
(* Goal: forall _ : @eq (@Tpoint Tn) P C1, @Col Tn C1 B1 B2 *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) P C1), @Col Tn C1 B1 B2 *)
    intro; subst C1; auto.
(* Goal: forall _ : @Col Tn P Q A1, @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
  intro.
(* Goal: @Col Tn C1 B1 B2 *)
  assert(HParAB : Par A1 A2 B1 B2).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    {
(* Goal: @Par Tn A1 A2 B1 B2 *)
    assert (Par_strict A1 A2 B1 B2); [|Par].
(* Goal: @Par_strict Tn A1 A2 B1 B2 *)
    apply (par_not_col_strict _ _ _ _ P); Col.
(* Goal: @Par Tn A1 A2 B1 B2 *)
    apply par_symmetry.
(* Goal: @Par Tn B1 B2 A1 A2 *)
    destruct HPerp2 as [X [Y [HCol1 [HPerp1 HPerp2]]]].
(* Goal: @Par Tn B1 B2 A1 A2 *)
    assert (HI1 := HPerp1); assert (HI2 := HPerp2).
(* Goal: @Par Tn B1 B2 A1 A2 *)
    destruct HI1 as [I1 H1]; destruct HI2 as [I2 H2].
(* Goal: @Par Tn B1 B2 A1 A2 *)
    apply perp_in_col in H1; apply perp_in_col in H2.
(* Goal: @Par Tn B1 B2 A1 A2 *)
    destruct H1 as [HCol2 HCol3]; destruct H2 as [HCol4 HCol5].
(* Goal: @Par Tn B1 B2 A1 A2 *)
    assert (P = I2); [|treat_equalities; rename I1 into R].
(* Goal: @Coplanar Tn P Q A1 C1 *)
      {
      elim (perp_not_col2 _ _ _ _ (perp_sym _ _ _ _ HPerp2)); intro;
      [apply l6_21 with B1 B2 X Y|apply l6_21 with B1 B2 Y X]; assert_diffs; Col.
      }
(* Goal: @Par Tn B1 B2 A1 A2 *)
    elim (eq_dec_points P R); intro HNE; treat_equalities; [exfalso; Col|].
    apply (l12_9 _ _ _ _ X Y); Perp; apply coplanar_perm_16;
    apply col2_cop__cop with P R; try solve [assert_diffs; ColR];
    apply coplanar_perm_2;
    [apply col_cop__cop with A2|apply col_cop__cop with A1|
     apply col_cop__cop with A2|apply col_cop__cop with A1];
    Col; try solve [assert_diffs; auto]; apply coplanar_perm_16;
    [apply col_cop__cop with B2|apply col_cop__cop with B2|
     apply col_cop__cop with B1|apply col_cop__cop with B1];
    assert_diffs; Col; Cop.
    }
(* Goal: @Col Tn C1 B1 B2 *)
  elim(col_dec P A1 A2).
(* Goal: forall _ : @Col Tn P Q A1, @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
    { intro.
(* Goal: @Per Tn C1 P Q *)
      assert_diffs.
(* Goal: @Col Tn C1 B1 B2 *)
      apply (not_strict_par _ _ _ _ P) in HParAB; Col.
(* Goal: @Col Tn C1 B1 B2 *)
      apply (not_strict_par _ _ _ _ P) in HParAC; Col.
(* Goal: @Col Tn C1 B1 B2 *)
      spliter.
(* Goal: @Col Tn C1 B1 B2 *)
      ColR.
    }
(* Goal: forall _ : not (@Col Tn P A1 A2), @Col Tn C1 B1 B2 *)
    intro HStrict.
(* Goal: @Col Tn C1 B1 B2 *)
    apply (par_not_col_strict _ _ _ _ P) in HParAB; Col.
(* Goal: @Col Tn C1 B1 B2 *)
    apply (par_not_col_strict _ _ _ _ P) in HParAC; Col.
(* Goal: @Col Tn C1 B1 B2 *)
    destruct HPerp2 as [P1 [P2 [HP [HPerpAP HPerpBP]]]].
(* Goal: @Col Tn C1 B1 B2 *)
    assert(HQ := HPerpAP); auto.
(* Goal: @Col Tn C1 B1 B2 *)
    destruct HQ as [Q [_ [_ [HQP[HQL _]]]]].
(* Goal: @Col Tn C1 B1 B2 *)
    assert(HP' := HPerpBP); auto.
(* Goal: @Col Tn C1 B1 B2 *)
    destruct HP' as [P' HPerpP].
(* Goal: @Col Tn C1 B1 B2 *)
    assert(P'=P) by (apply (l8_14_2_1b _ P1 P2 B1 B2); Col).
(* Goal: @Col Tn C1 B1 B2 *)
    subst P'.
(* Goal: @Col Tn C1 B1 B2 *)
    destruct HPerpP as [_ [_ [HPP _]]].
(* Goal: @Col Tn C1 B1 B2 *)
    assert(P<>Q) by (intro; subst Q; auto).
(* Goal: @Col Tn C1 B1 B2 *)
    apply (perp_col0 _ _ _ _ P Q) in HPerpAP; Col.
(* Goal: @Col Tn C1 B1 B2 *)
    apply (perp_col0 _ _ _ _ P Q) in HPerpBP; Col.
(* Goal: @Col Tn C1 B1 B2 *)
    clear dependent P1.
(* Goal: @Col Tn C1 B1 B2 *)
    clear dependent P2.

    assert(~ Col Q C1 P)
      by (apply (par_not_col A1 A2); auto;
          apply (par_strict_col_par_strict _ _ _ C2); Col).
(* Goal: @Per Tn C1 P Q *)
    assert_diffs.
(* Goal: @Col Tn C1 B1 B2 *)
    assert(HB3 : exists B3, Col B1 B2 B3 /\ B3 <> P).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    { elim(eq_dec_points B1 P).
(* Goal: forall _ : @eq (@Tpoint Tn) B1 P, @ex (@Tpoint Tn) (fun B3 : @Tpoint Tn => and (@Col Tn B1 B2 B3) (not (@eq (@Tpoint Tn) B3 P))) *)
(* Goal: forall _ : not (@eq (@Tpoint Tn) B1 P), @ex (@Tpoint Tn) (fun B3 : @Tpoint Tn => and (@Col Tn B1 B2 B3) (not (@eq (@Tpoint Tn) B3 P))) *)
      intro; subst B1; exists B2; Col.
(* Goal: forall _ : not (@eq (@Tpoint Tn) B1 P), @ex (@Tpoint Tn) (fun B3 : @Tpoint Tn => and (@Col Tn B1 B2 B3) (not (@eq (@Tpoint Tn) B3 P))) *)
      intro; exists B1; Col.
    }
(* Goal: @Col Tn C1 B1 B2 *)
    destruct HB3 as [B3 []].
(* Goal: @Col Tn C1 B1 B2 *)
    assert(Col P C1 B3); [|ColR].
(* Goal: @Per Tn C1 P Q *)
    assert_diffs.
(* Goal: @Col Tn P C1 B3 *)
    apply (cop_perp2__col _ _ _ P Q); auto; [| |apply (perp_col2 B1 B2); Col].
(* Goal: @Coplanar Tn P Q C1 B3 *)
(* Goal: @Perp Tn P C1 P Q *)
    assert (Coplanar A1 A2 P B3) by (apply col2_cop__cop with B1 B2; Col; Cop).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    assert (Coplanar A1 A2 C1 C2) by (apply pars__coplanar; auto).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    assert (Coplanar A1 A2 P C1) by (apply col2_cop__cop with C1 C2; Col; Cop).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    assert (Coplanar A1 A2 P Q) by (apply coplanar_perm_1, col__coplanar; Col).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    CopR.
(* Goal: @Perp Tn P C1 P Q *)
    apply perp_left_comm.
(* Goal: @Perp Tn C1 P P Q *)
    apply per_perp; auto.

(* Goal: @Per Tn C1 P Q *)
    assert(HA3 : exists A3, Col A1 A2 A3 /\ TS P Q C1 A3).
(* Goal: @Coplanar Tn P Q A1 C1 *)
    { elim(col_dec P Q A1);
      [|intro; apply (cop_not_par_other_side _ _ _ _ Q); Col].

(* Goal: @Coplanar Tn P Q A1 C1 *)
      {
(* Goal: forall _ : @Col Tn P Q A1, @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
      intro.
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
      assert(HA3 := cop_not_par_other_side P Q A2 A1 Q C1).
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
      destruct HA3 as [A3 []]; Col; [intro; apply HStrict; ColR| |].
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 C1 C2) by (apply pars__coplanar; auto).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 P C1) by (apply col2_cop__cop with C1 C2; Col; Cop).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 P Q) by (apply coplanar_perm_1, col__coplanar; Col).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      CopR.
(* Goal: @ex (@Tpoint Tn) (fun A3 : @Tpoint Tn => and (@Col Tn A1 A2 A3) (@TS Tn P Q C1 A3)) *)
      exists A3; split; Col.
      }

(* Goal: @Coplanar Tn P Q A1 C1 *)
      {
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 C1 C2) by (apply pars__coplanar; auto).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 P C1) by (apply col2_cop__cop with C1 C2; Col; Cop).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      assert (Coplanar A1 A2 P Q) by (apply coplanar_perm_1, col__coplanar; Col).
(* Goal: @Coplanar Tn P Q A1 C1 *)
      CopR.
      }

    }
(* Goal: @Per Tn C1 P Q *)
    destruct HA3 as [A3 [HA3 Hts]].
(* Goal: @Per Tn C1 P Q *)
    assert(~ Col A3 P Q) by (destruct Hts as [_ []]; auto).
(* Goal: @Per Tn C1 P Q *)
    assert_diffs.
(* Goal: @Per Tn C1 P Q *)
    apply (l11_17 A3 Q P).
(* Goal: @Per Tn A3 Q P *)
(* Goal: @CongA Tn A3 Q P C1 P Q *)
    apply perp_per_1; auto; apply (perp_col2 A1 A2); Col.
(* Goal: @CongA Tn A3 Q P C1 P Q *)
    apply conga_sym.
(* Goal: @CongA Tn C1 P Q A3 Q P *)
    apply aip; auto.
(* Goal: @Par Tn P C1 Q A3 *)
    apply (par_col4__par C1 C2 A1 A2); Col.
(* Goal: @Par Tn C1 C2 A1 A2 *)
    apply par_strict_par; Par.
Qed.

Lemma alternate_interior__playfair_bis : alternate_interior_angles_postulate -> alternative_playfair_s_postulate.
Proof.
(* Goal: forall _ : @alternate_interior_angles_postulate Tn, @alternative_playfair_s_postulate Tn *)
intros aia.
(* Goal: @alternative_playfair_s_postulate Tn *)
intros A1 A2 B1 B2 C1 C2 P HPerp2 HPB HCop HParAC HPC.
(* Goal: forall _ : @Col Tn P C1 C2, and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
split.
(* Goal: @Col Tn C1 B1 B2 *)
(* Goal: @Col Tn C2 B1 B2 *)
apply (alternate_interior__playfair_aux aia A1 A2 _ _ _ C2 P); auto.
(* Goal: @Col Tn C2 B1 B2 *)
apply (alternate_interior__playfair_aux aia A1 A2 _ _ _ C1 P); Col; Par.
Qed.

End alternate_interior_angles_playfair_bis.