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

Section playfair_par_trans.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** This is Legendre theorem XXV http://gallica.bnf.fr/ark:/12148/bpt6k202689z/f29.image *)

Lemma playfair_implies_par_trans :
  playfair_s_postulate -> postulate_of_transitivity_of_parallelism.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, @postulate_of_transitivity_of_parallelism Tn *)
  intros HP A1 A2 B1 B2 C1 C2 HAB HBC.
(* Goal: @Par Tn A1 A2 C1 C2 *)
  assert_diffs.
(* Goal: @Par Tn A1 A2 C1 C2 *)
  destruct (cop_dec A1 A2 C1 B1) as [|HNCop]; [induction (col_dec A1 A2 C1)|].

  - right.
(* Goal: and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) C1 C2)) (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) *)
    destruct (HP B1 B2 C1 C2 A1 A2 C1); Par; Col.

  - left.
(* Goal: @Par_strict Tn A1 A2 C1 C' *)
    repeat split; auto.
(* Goal: @Par_strict Tn B1 B2 C1 C' *)
(* Goal: @Col Tn C1 C' C2 *)
    { apply par_symmetry in HBC.
(* Goal: @Coplanar Tn A1 A2 C1 C2 *)
      destruct HBC; [destruct HAB|]; [|spliter..].
      - assert_ncols; apply coplanar_pseudo_trans with B1 B2 C1; [Col| | |Cop..];
          apply coplanar_pseudo_trans with A1 A2 B1; Col; Cop.
      - apply coplanar_perm_16, col2_cop__cop with B1 B2; Col; Cop.
      - apply col2_cop__cop with B1 B2; Col; Cop.
    }
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C'))) *)
    intros [X []].
(* Goal: False *)
    destruct (HP B1 B2 A1 A2 C1 C2 X); Par; Col.

  - apply (par_not_col_strict A1 A2 B1 B2 B1) in HAB; [|Col|intro; apply HNCop; Cop].
    apply (par_not_col_strict B1 B2 C1 C2 C1) in HBC;
      [|Col|intro; apply HNCop, coplanar_perm_1, col_cop__cop with B2; Cop].
(* Goal: @Par Tn A1 A2 C1 C2 *)
    destruct (cop_osp__ex_cop2 A1 A2 C1 B1 B2 C1) as [C' [HCop1 [HCop2 HC1C']]]; Cop.
(* Goal: @OSP Tn A1 A2 C1 B1 B2 *)
(* Goal: @Par Tn A1 A2 C1 C2 *)
      apply cop2_os__osp with A1 A2; Cop; Side.
    assert (HC' : forall X, Coplanar A1 A2 B1 X -> ~ Col X C1 C').
(* Goal: @Par_strict Tn B1 B2 C1 C' *)
(* Goal: @Col Tn C1 C' C2 *)
    { intros X HX1 HX2.
(* Goal: False *)
      apply (par_not_col A1 A2 B1 B2 X HAB).
      - apply (l9_30 A1 A2 C1 A1 A2 B1 B1); Cop.
(* Goal: not (@Col Tn A1 A2 B1) *)
(* Goal: @Coplanar Tn A1 A2 C1 X *)
          apply par_strict_not_col_1 with B2, HAB.
(* Goal: @Coplanar Tn B1 B2 C1 X *)
        apply col_cop__cop with C'; Col.
      - apply (l9_30 A1 A2 B1 B1 B2 C1 C1); Cop.
(* Goal: not (@Col Tn B1 B2 C1) *)
(* Goal: @Coplanar Tn B1 B2 C1 X *)
          apply par_strict_not_col_1 with C2, HBC.
(* Goal: @Coplanar Tn B1 B2 C1 X *)
        apply col_cop__cop with C'; Col.
    }
(* Goal: @Par Tn A1 A2 C1 C2 *)
    left; apply par_strict_col_par_strict with C'; auto.
(* Goal: @Par_strict Tn A1 A2 C1 C' *)
    { repeat split; auto.
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C'))) *)
      intros [X []].
(* Goal: False *)
      apply HC' with X; Cop.
    }
(* Goal: @Col Tn C1 C' C2 *)
    assert (HBC' : Par_strict B1 B2 C1 C').
(* Goal: @Par_strict Tn B1 B2 C1 C' *)
(* Goal: @Col Tn C1 C' C2 *)
    { repeat split; Col.
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C'))) *)
      intros [X []].
(* Goal: False *)
      apply HC' with X; trivial.
(* Goal: @Coplanar Tn A1 A2 B1 X *)
      apply col_cop__cop with B2; Col; Cop.
    }
(* Goal: @Col Tn C1 C' C2 *)
    destruct (HP B1 B2 C1 C2 C1 C' C1); Par; Col.
Qed.

End playfair_par_trans.
