Library GeoCoq.Meta_theory.Parallel_postulates.proclus_bis_proclus

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

Section proclus_bis_proclus.

Context `{T2D:Tarski_2D}.

Lemma proclus_bis__proclus : alternative_proclus_postulate → proclus_postulate.
Proof.
  intros proclus_bis A B C D P Q HPar HInter HNCol.
  elim(Col_dec C D P).
    intro; ∃ P; Col.
  intro HNCol1.
  apply par_symmetry in HPar.
  apply (par_not_col_strict _ _ _ _ P) in HPar; auto.
  assert(HC0 := l8_18_existence C D P).
  destruct HC0 as [C0 []]; auto.
  assert(HNCol2 : ¬ Col C0 A B) by (apply (par_not_col C D); Col).
  assert_diffs.
  assert(HA0 : ∃ A0, Col A B A0 ∧ ¬ Col C0 P A0).
  { elim(Col_dec C0 P A).
    - intro.
      assert(¬ Col C0 P B) by (intro; apply HNCol2; ColR).
      ∃ B.
      split; Col.

    - intro.
      ∃ A.
      split; Col.
  }
  destruct HA0 as [A0 []].
  assert(HA' := l10_15 C0 P P A0).
  destruct HA' as [A' []]; Col.
  assert_diffs.
  elim(Col_dec A0 P A').
  - intro.
    apply (proclus_bis A0 P); Col.
    2: intro; apply HNCol; ColR.
    ∃ C0.
    ∃ P.
    split; Col.
    split.
    2: Perp.
    apply perp_right_comm.
    apply (perp_col1 _ _ _ A'); Perp; Col.

  - intro.
    exfalso.
    assert(HY := proclus_bis A' P C D P A0).
    destruct HY as [Y []]; Col.
      ∃ C0; ∃ P; repeat split; Col; Perp.
    assert(Habs : ¬ Col Y A B) by (apply (par_not_col C D); Col).
    apply Habs; ColR.
Qed.

End proclus_bis_proclus.