Library GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg


Require Export GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal.

Section Desargues_Hessenberg.

Context `{TE:Tarski_2D_euclidean}.

Lemma l13_15_1 : A B C A' B' C' O ,
  ¬ Col A B C ¬ Par O B A C
  Par_strict A B A' B' Par_strict A C A' C'
  Col O A A' Col O B B' Col O C C'
  Par B C B' C'.
Proof.
    intros.
    assert(¬Col B A' B').
      intro.
      apply H1.
       B.
      split; Col.
    assert(¬Col A A' B').
      intro.
      apply H1.
       A.
      split; Col.
    assert(B O).
      intro.
      subst B.
      apply H1.
       A'.
      split; Col.
    assert(A O).
      intro.
      subst A.
      apply H1.
       B'.
      split; Col.
    assert(¬ Col A' A C).
      eapply (par_not_col A' C').
        Par.
      Col.
    assert(C O).
      intro.
      subst C.
      apply H10.
      Col.
    assert(¬Col O A B).
      intro.
      apply H1.
       O.
      split.
        Col.
      assert(Col O A B').
        apply (col_transitivity_1 _ B); Col.
      apply (col_transitivity_1 _ A); Col.
    assert(¬Col O A C).
      intro.
      apply H2.
       O.
      split.
        Col.
      assert(Col O A C').
        apply (col_transitivity_1 _ C); Col.
      apply (col_transitivity_1 _ A); Col.
    assert(¬ Col A' B' C').
      intro.
      apply H.
      assert(Par A' C' A B).
        apply(par_col_par_2 A' B' A B C').
          intro.
          subst C'.
          unfold Par_strict in H2.
          tauto.
          auto.
        left.
        Par.
      assert(Par A C A B).
        apply(par_trans A C A' C'); Par.
      induction H16.
        apply False_ind.
        apply H16.
         A.
        split; Col.
      spliter; Col.
    induction(Col_dec O B C).
      right.
      repeat split.
        intro.
        subst C.
        apply H.
        Col.
        intro.
        subst C'.
        apply H14.
        Col.
        assert(Col O B C').
          apply (col_transitivity_1 _ C); Col.
        apply (col_transitivity_1 _ O); Col.
      assert(Col O C B').
        apply (col_transitivity_1 _ B); Col.
      apply (col_transitivity_1 _ O); Col.
    assert(B' O).
      intro.
      subst B'.
      apply H7.
      Col.
    assert(B' O).
      intro.
      subst B'.
      apply H7.
      Col.
    assert(A' O).
      intro.
      subst A'.
      apply H6.
      Col.
    assert(¬ Col A A' C').
      eapply (par_not_col A C).
        Par.
      Col.
    assert(C' O).
      intro.
      subst C'.
      apply H19.
      Col.
    assert(¬Col O A' B').
      intro.
      apply H1.
       O.
      split.
        assert(Col O A' B).
          apply (col_transitivity_1 _ B'); Col.
        apply (col_transitivity_1 _ A'); Col.
      Col.
    assert(¬Col O A' C').
      intro.
      apply H2.
       O.
      split.
        ColR.
      Col.
    assert(¬Col B' A B).
      intro.
      apply H1.
       B'.
      Col.
    assert(¬Col A' A B).
      intro.
      apply H1.
       A'.
      split; Col.
    assert( C : Tpoint, D : Tpoint, C D Par O B C D Col A C D).
      apply(parallel_existence O B A).
      auto.
    ex_and H25 X.
    ex_and H26 Y.
    assert( L : Tpoint, Col L X Y Col L A' C').
      apply(not_par_inter_exists X Y A' C').
      intro.
      apply H0.
      eapply (par_trans O B X Y).
        auto.
      apply par_symmetry.
      apply (par_trans A C A' C').
        left.
        auto.
      Par.
    ex_and H28 L.
    assert(A L).
      intro.
      subst L.
      contradiction.
    assert(Par A L O B').
      apply par_symmetry.
      apply(par_col_par_2 _ B); Col.
      apply par_symmetry.
      apply par_left_comm.
      induction(eq_dec_points X L).
        subst X.
        apply (par_col_par_2 _ Y); Col.
        Par.
      apply (par_col_par_2 _ X); try auto.
        ColR.
      apply par_left_comm.
      apply (par_col_par_2 _ Y); Col.
      Par.
    assert(¬ Par X Y O C).
      intro.
      assert(Par O B O C).
        apply (par_trans O B X Y); Par.
      induction H33.
        apply H33.
         O.
        split; Col.
      spliter.
      apply H15.
      Col.
    assert(HH:=not_par_inter_exists X Y O C H32).
    ex_and HH M.
    assert(A M).
      intro.
      subst M.
      apply H13.
      Col.
    assert(Par O B A M).
      apply (par_col_par_2 _ B'); Col.
      apply par_symmetry.
      apply (par_col_par_2 _ L); try auto.
      ColR.
    assert(L A').
      intro.
      subst L.
      clean_trivial_hyps.
      apply H12.
      induction(eq_dec_points A' X).
        subst X.
        assert(Par A' A O B).
          apply (par_col_par_2 _ Y); Col.
          Par.
        induction H29.
          apply False_ind.
          apply H29.
           O.
          split; Col.
        spliter.
        ColR.
      assert(Par X A' O B).
        apply (par_col_par_2 _ Y); Col.
        Par.
      assert(Par A' A O B).
        apply (par_col_par_2 _ X); try auto.
          ColR.
        Par.
      induction H38.
        apply False_ind.
        apply H38.
         O.
        split; Col.
      spliter.
      Col.
    assert(¬ Par L B' A' B').
      intro.
      induction H38.
        apply H38.
         B'.
        split;Col.
      spliter.
      apply H14.
      eapply (col_transitivity_1 _ L); Col.
    assert(¬ Par A B L B').
      apply(par_not_par A' B' A B L B').
        left.
        Par.
      intro.
      apply H38.
      Par.
    assert(HH:=not_par_inter_exists A B L B' H39 ).
    ex_and HH N.
    assert(Par_strict A L O B').
      induction H31.
        auto.
      spliter.
      apply False_ind.
      apply H12.
      apply (col_transitivity_1 _ B'); Col.
    assert(A N).
      intro.
      subst N.
      apply H42.
       B'; Col.
    assert(Par A N A' B').
      apply (par_col_par_2 _ B); Col.
      left.
      Par.
    clean_duplicated_hyps.
    assert(Par O N L A').
      induction(Par_dec A O N L).
        assert(Par_strict A O N L).
          induction H17.
            auto.
          spliter.
          apply False_ind.
          apply H23.
          assert(Col N A B').
            eapply (col_transitivity_1 _ L); Col.
          apply col_permutation_2.
          eapply (col_transitivity_1 _ N); Col.
        apply(l13_14 A O A' A N L N B'); Col.
          Par.
        Par.
      assert(N L).
        intro.
        subst L.
        apply H42.
         B.
        split; Col.
      assert(HH:=not_par_inter_exists A O N L H17).
      ex_and HH P.
      apply par_right_comm.
      assert(P L).
        intro.
        subst P.
        apply H42.
         O.
        split; Col.
      assert(P O).
        intro.
        subst P.
        apply H42.
         L.
        split.
          Col.
        apply (col_transitivity_1 _ N); Col.
      assert(L B').
        intro.
        subst L.
        apply H42.
         B'.
        split; Col.
      assert(A P).
        intro.
        subst P.
        assert(Col A B L).
          apply (col_transitivity_1 _ N); Col.
        assert(Col L A B').
          apply (col_transitivity_1 _ N); Col.
        apply H39.
        apply par_symmetry.
        right.
        repeat split.
          assumption.
          intro.
          subst B.
          apply H23.
          Col.
          Col.
        ColR.
      assert(P N).
        intro.
        subst P.
        apply H12.
        apply col_permutation_2.
        apply (col_transitivity_1 _ N); Col.
      assert(A' P).
        intro.
        subst P.
        apply H38.
        right.
        repeat split; try assumption.
          intro.
          subst B'.
          apply H21.
          Col.
          ColR.
        Col.
      assert(B' P).
        intro.
        subst P.
        apply H21.
        apply (col_transitivity_1 _ A); Col.
      apply(l13_11 O A' A L N B' P); Par; try ColR.
      intro.
      apply H42.
       L.
      split.
        Col.
      assert(Col L O N).
        apply (col_transitivity_1 _ P); Col.
      apply (col_transitivity_1 _ N); Col.
    assert(Par A' C' O N).
      apply (par_col_par_2 _ L).
        intro.
        subst C'.
        apply H22.
        Col.
        Col.
      Par.
    assert(Par O N A C).
      apply (par_trans _ _ A' C'); Par.
    assert(Par N M B C).
      induction(Par_dec A N O C).
        assert(Par_strict A N O C).
          induction H47.
            auto.
          spliter.
          apply False_ind.
          apply H13.
          Col.
        apply par_right_comm.
        apply(l13_14 A N B A O C M O ); Par; Col.
      assert(HH:= not_par_inter_exists A N O C H47).
      ex_and HH P.
      assert(B P).
        intro.
        subst P.
        apply H15.
        Col.
      assert(A P).
        intro.
        subst P.
        apply H13.
        Col.
      assert(M P).
        intro.
        subst P.
        induction H36.
          apply H36.
           B.
          split.
            Col.
          apply col_permutation_2.
          apply (col_transitivity_1 _ N); Col.
        spliter.
        apply H12.
        apply col_permutation_2.
        apply (col_transitivity_1 _ M); Col.
      assert(O P).
        intro.
        subst P.
        induction H46.
          apply H46.
           A.
          split; Col.
        spliter.
        apply H13.
        Col.
      assert(P N).
        intro.
        subst P.
        induction H46.
          apply H46.
           C.
          split; Col.
        spliter.
        apply H13.
        Col.
      apply(l13_11 N B A C M O P); Par; try ColR.
      intro.
      assert(Col N A C) by ColR.
      apply H.
      ColR.
    assert(Par N M B' C').
      induction(Par_dec N B' O C').
        assert(Par_strict N B' O C').
          induction H48.
            auto.
          spliter.
          apply False_ind.
          induction H46.
            apply H46.
             C.
            split.
              ColR.
            Col.
          spliter.
          contradiction.
        assert(M L).
          intro.
          subst M.
          apply H49.
           L.
          split.
            Col.
          apply col_permutation_2.
          apply(col_transitivity_1 _ C); Col.
        assert(L C').
          intro.
          subst C'.
          apply H49.
           L.
          split; Col.
        assert(Par L M O B').
          apply (par_col_par_2 _ A); try assumption.
            auto.
            ColR.
          Par.
        assert(Par L C' O N).
          apply (par_col_par_2 _ A'); Col.
          Par.
        apply par_right_comm.
        apply(l13_14 B' N B' L O C' M O);sfinish.
      assert(HH:= not_par_inter_exists N B' O C' H48).
      ex_and HH P.
      assert(B' P).
        intro.
        subst P.
        apply H15.
        ColR.
      induction(eq_dec_points C' L).
        subst L.
        assert(C' = M).
          induction (Col_dec O X C).
            apply (l6_21 O C Y X).
              intro.
              assert(Col O X Y) by ColR.
              induction H26.
                apply H26.
                 O.
                split; Col.
              spliter.
              apply H12.
              apply(col3 X Y); Col.
              auto.
              Col.
              Col.
              Col.
              Col.
          apply (l6_21 O C X Y); Col.
        subst M.
        right.
        repeat split; try auto.
          intro.
          subst N.
          apply par_distincts in H47; spliter; auto.
          intro; subst; apply H14; Col.
          Col.
        Col.
      assert(L P).
        intro.
        subst P.
        apply H22.
        apply col_permutation_1.
        apply (col_transitivity_1 _ L); Col.
      induction (eq_dec_points L M).
        subst L.
        assert(C' = M).
          apply (l6_21 O C A' C'); Col.
            intro.
            apply H22.
            ColR.
            intro.
            subst C'.
            apply H22.
            Col.
            subst M.
            right.
            repeat split; try auto. Col. Col.
              assert(Par L M O B').
            apply (par_col_par_2 _ A); try assumption. ColR.
              Par.
            assert(Par L C' N O).
              apply (par_col_par_2 _ A'); Col.
              Par.
            assert(B' N).
              intro.
              subst N.
              contradiction.
            apply(l13_11 N B' L C' M O P); Par.
              intro.
              assert(Col P B' C').
                apply (col_transitivity_1 _ N).
                  intro.
                  subst N.
                  induction H45.
                    apply H45.
                     C'.
                    split; Col.
                  spliter.
                  apply H22.
                  ColR.
                  Col.
                Col.
              assert(Col C' O B' ).
                apply (col_transitivity_1 _ P).
                  intro.
                  subst P.
                  clean_trivial_hyps.
                  assert(Col B' C' L).
                    apply (col_transitivity_1 _ N); Col.
                  apply H14.
                  ColR.
                  Col.
                Col.
              assert(Col O B C').
                apply (col_transitivity_1 _ B'); Col.
              apply H15.
              ColR.
              ColR.
              intro.
              subst M.
              assert(Col B' P L).
                apply (col_transitivity_1 _ N); Col.
              assert(Col L A B').
                assert(Col P A L).
                  apply (col3 X Y); Col.
                apply (col_transitivity_1 _ P); Col.
              apply H42.
               B'.
              split; Col.
              intro.
              subst P.
              assert(N = B).
                apply (l6_21 A B O B'); Col.
                  subst N.
                  induction H47.
                    apply H47.
                     B.
                    split; Col.
                  spliter.
                  assert(B = O).
                    apply (l6_21 O B' M C); Col.
                  subst B.
                  induction H56.
                    apply H56.
                     L.
                    split; Col.
                  tauto.
                  ColR.
                  ColR.
                  apply (par_trans _ _ N M); Par.
              Qed.

Lemma l13_15_2_aux : A B C A' B' C' O , ¬Col A B C
                                          ¬Par O A B C
                                          Par O B A C
                                          Par_strict A B A' B'
                                          Par_strict A C A' C'
                                          Col O A A' Col O B B' Col O C C'
                                          Par B C B' C'.
Proof.
    intros.
    assert(¬Col O A B ¬Col O B C ¬Col O A C).
      induction H1; repeat split; intro.
        apply H1.
         A.
        split; Col.
        apply H1.
         C.
        split; Col.
        apply H1.
         O.
        split; Col.
        spliter.
        apply H; Col.
        spliter.
        apply H; Col.
      spliter.
      apply H; Col.
    spliter.
    assert( A O B O C O).
      repeat split; intro; subst O.
        apply H9.
        Col.
        apply H8.
        Col.
      apply H9.
      Col.
    spliter.
    assert( A' O).
      intro.
      subst A'.
      assert(Par O B A B).
        apply (par_col_par_2 _ B'); Col.
        left.
        Par.
      induction H13.
        apply H13.
         B.
        split; Col.
      spliter.
      contradiction.
    assert(B' O).
      intro.
      subst B'.
      assert(Par O A B A).
        apply(par_col_par_2 _ A'); Col.
        apply par_comm.
        apply par_symmetry.
        left.
        Par.
      induction H14.
        apply H14.
         A.
        split; Col.
      spliter.
      apply H7.
      Col.
    assert(C' O).
      intro.
      subst C'.
      assert(Par O A C A).
        apply (par_col_par_2 _ A'); Col.
        apply par_comm.
        apply par_symmetry.
        left.
        Par.
      induction H15.
        apply H15.
         A.
        split; Col.
      spliter.
      apply H9.
      Col.
    assert(¬Col O A' B').
      intro.
      assert(Col O A B').
        apply (col_transitivity_1 _ A'); Col.
      apply H7.
      apply (col_transitivity_1 _ B'); Col.
    assert(¬Col O B' C').
      intro.
      assert(Col O B C').
        apply (col_transitivity_1 _ B'); Col.
      apply H8.
      apply (col_transitivity_1 _ C'); Col.
    assert(¬Col O A' C').
      intro.
      assert(Col O A C').
        apply (col_transitivity_1 _ A'); Col.
      apply H9.
      apply (col_transitivity_1 _ C'); Col.
    assert(A A').
      intro.
      subst A'.
      apply H3.
       A.
      split; Col.
    assert(B B').
      intro.
      subst B'.
      apply H2.
       B.
      split; Col.
    assert(C C').
      intro.
      subst C'.
      apply H3.
       C.
      split; Col.
    induction(Par_dec B C B' C').
      auto.
    assert(B C).
      intro.
      subst C.
      apply H.
      Col.
    assert(HP:=parallel_existence B C B' H23).
    ex_and HP X.
    ex_and H24 Y.
    assert(¬Par X Y O C).
      intro.
      assert(Par O C B C).
        apply (par_trans _ _ X Y); Par.
      induction H28.
        apply H28.
         C.
        split; Col.
      spliter.
      contradiction.
    assert(HH:=not_par_inter_exists X Y O C H27).
    ex_and HH C''.
    assert(B' C'').
      intro.
      subst C''.
      assert(Col O B C).
        apply (col_transitivity_1 _ B'); Col.
      contradiction.
    assert(Par B' C'' B C ).
      induction(eq_dec_points B' X).
        subst X.
        apply (par_col_par_2 _ Y).
          auto.
          Col.
        Par.
      apply (par_col_par_2 _ X).
        auto.
        apply col_permutation_2.
        apply(col_transitivity_1 _ Y); Col.
      apply par_left_comm.
      apply (par_col_par_2 _ Y); Col.
      Par.
    assert(Par A C A' C'').
      eapply(l13_15_1 B A C B' A' C'' O); Col.
        apply par_strict_comm.
        auto.
      induction H31.
        Par.
      spliter.
      apply False_ind.
      apply H8.
      apply col_permutation_2.
      apply(col_transitivity_1 _ B'); Col.
    assert(C' C'').
      intro.
      subst C''.
      apply H22.
      Par.
    assert(Par A' C' A' C'').
      apply (par_trans _ _ A C).
        left.
        Par.
      Par.
    assert(C' = C'').
      apply (l6_21 A' C' O C); Col.
        induction H34.
        apply False_ind.
        apply H34.
         A'.
        split; Col.
        spliter.
        Col.
    contradiction.
Qed.

Lemma l13_15_2 : A B C A' B' C' O , ¬Col A B C
                                          Par O B A C
                                          Par_strict A B A' B'
                                          Par_strict A C A' C'
                                          Col O A A' Col O B B' Col O C C'
                                          Par B C B' C'.
Proof.
    intros.
    induction(Par_dec B C B' C').
      auto.
    assert(HH:=not_par_one_not_par B C B' C' O A H6).
    induction HH.
      apply (l13_15_2_aux A B C A' B' C' O); auto.
      intro.
      apply H7.
      Par.
    apply par_symmetry.
    assert(¬ Col A' B' C').
      intro.
      apply H.
      assert(Par A' B' A' C').
        right.
        repeat split; Col.
          intro.
          subst B'.
          apply H1.
           A.
          split; Col.
        intro.
        subst C'.
        apply H2.
         A.
        split; Col.
      assert(Par A B A C).
        apply(par_trans _ _ A' B').
          left.
          auto.
        apply(par_trans _ _ A' C').
          Par.
        left.
        Par.
      induction H10.
        apply False_ind.
        apply H10.
         A.
        split; Col.
      spliter.
      Col.
    assert(B' O).
      intro.
      subst B'.
      assert(Par O A B A).
        apply (par_col_par_2 _ A'); Col.
          intro.
          subst A.
          apply H1.
           O.
          split; Col.
        apply par_comm.
        left.
        Par.
      induction H9.
        apply H9.
         A.
        split; Col.
      spliter.
      apply H1.
       O.
      split; Col.
    assert(Par O B O B').
      right.
      repeat split; Col.
      intro.
      subst B.
      apply par_distincts in H0.
      tauto.
    apply (l13_15_2_aux A' B' C' A B C O); Col; Par.
      intro.
      apply H7.
      apply par_symmetry.
      apply (par_col_par_2 _ A').
        intro.
        subst A.
        induction H0.
          apply H0.
           O.
          split; Col.
        spliter.
        apply H.
        Col.
        Col.
      Par.
    apply (par_trans _ _ O B).
      Par.
    apply (par_trans _ _ A C).
      Par.
    left.
    Par.
Qed.

Lemma l13_15 : A B C A' B' C' O , ¬Col A B C
                                          Par_strict A B A' B'
                                          Par_strict A C A' C'
                                          Col O A A' Col O B B' Col O C C'
                                          Par B C B' C'.
Proof.
    intros.
    induction(Par_dec O B A C).
      apply (l13_15_2 A B C A' B' C' O); Col; Par.
    apply (l13_15_1 A B C A' B' C' O); Col; Par.
Qed.

Lemma l13_15_par : A B C A' B' C', ¬Col A B C
                                          Par_strict A B A' B'
                                          Par_strict A C A' C'
                                          Par A A' B B'
                                          Par A A' C C'
                                          Par B C B' C'.
Proof.
    intros.
    assert(Plg B' A' A B).
      apply(pars_par_plg B' A' A B).
        apply par_strict_left_comm.
        Par.
      Par.
    apply plg_to_parallelogram in H4.
    apply plg_permut in H4.
    assert(Plg A' C' C A).
      apply(pars_par_plg A' C' C A).
        apply par_strict_right_comm.
        Par.
      Par.
    apply plg_to_parallelogram in H5.
    apply plg_permut in H5.
    assert(Parallelogram B B' C' C B = B' A' = A C = C' B = C).
      apply(plg_pseudo_trans B B' A' A C C').
        apply plg_sym.
        auto.
      apply plg_comm2.
      apply plg_permut.
      apply plg_permut.
      auto.
    assert(Par B B' C C').
      apply (par_trans _ _ A A'); Par.
    induction H7.
      induction H6.
        assert(B B').
          apply par_distincts in H2.
          tauto.
        apply plg_par in H6.
          spliter.
          Par.
          auto.
        intro.
        subst C'.
        apply H7.
         B'.
        split; Col.
      spliter.
      subst C.
      subst C'.
      apply False_ind.
      apply H7.
       B.
      split; Col.
    induction H6.
      apply plg_par in H6.
        spliter.
        Par.
        spliter.
        auto.
      spliter.
      intro.
      subst C'.
      assert(Par A B A C).
        apply (par_trans _ _ A' B'); left; Par.
      induction H11.
        apply H11.
         A.
        split; Col.
      spliter.
      apply H.
      Col.
    spliter.
    subst B'.
    subst A'.
    subst C'.
    subst C.
    apply False_ind.
    apply H1.
     A.
    split; Col.
Qed.

Lemma l13_18_2 : A B C A' B' C' O, ¬Col A B C
                                Par_strict A B A' B'
                                Par_strict A C A' C'
                                (Par_strict B C B' C' Col O A A' Col O B B' Col O C C').
Proof.
    intros.
    spliter.
    assert(¬ Col O A B).
      intro.
      apply H0.
       O.
      split.
        Col.
      apply(col_transitivity_1 _ A); Col.
        intro.
        subst A.
        apply H0.
         B'.
        split; Col.
      apply(col_transitivity_1 _ B); Col.
      intro.
      subst B.
      apply H0.
       A'.
      split; Col.
    assert( Y : Tpoint, Col O C Y Col B' C' Y).
      apply(par_inter B C B' C' O C C); Col.
        left.
        Par.
      intro.
      induction H6.
        apply H6.
         C.
        split; Col.
      spliter.
      apply H2.
       B'.
      split;Col.
      apply col_permutation_2.
      apply (col_transitivity_1 _ O); Col.
      intro.
      subst O.
      apply H0.
       A'.
      split; Col.
    ex_and H6 C''.
    induction(Col_dec O C C').
      auto.
    apply False_ind.
    assert(Par C' C'' B C ).
      apply (par_col_par_2 _ B').
        intro.
        subst C''.
        contradiction.
        Col.
      apply par_left_comm.
      left.
      Par.
    assert(Par_strict C' C'' B C).
      induction H9.
        auto.
      spliter.
      apply False_ind.
      apply H8.
      apply col_permutation_2.
      apply (col_transitivity_1 _ C'').
        intro.
        subst C''.
        apply H2.
         C.
        split; Col.
        apply (col_transitivity_1 _ B); Col.
      Col.
    assert(¬Col O B C).
      intro.
      apply H10.
       B'.
      split; Col.
      apply col_permutation_2.
      apply (col_transitivity_1 _ O); Col.
      intro.
      subst B.
      apply H5.
      Col.
    assert(Par B' C'' B C).
      apply (par_col_par_2 _ C') ; Col.
        intro.
        subst B'.
        apply H11.
        apply(col_transitivity_1 _ C''); Col.
        intro.
        subst C''.
        apply H0.
         A.
        split; Col.
      left.
      Par.
    assert(Par_strict B' C'' B C).
      induction H12.
        auto.
      spliter.
      apply False_ind.
      apply H11.
      apply col_permutation_2.
      apply (col_transitivity_1 _ B'); Col.
      intro.
      subst B'.
      apply H2.
       B.
      split; Col.
    assert(Par A C A' C'').
      apply(l13_15 B A C B' A' C'' O); Par.
      intro.
      apply H.
      Col.
    assert(Par A' C' A' C'').
      apply (par_trans _ _ A C).
        left.
        Par.
      Par.
    induction H15.
      apply H15.
       A'.
      split; Col.
    spliter.
    assert(¬ Col A' B' C').
      intro.
      apply H.
      apply(col_par_par_col A' B' C' A B C H19); left; Par.
    assert( C' = C'').
      apply(l6_21 A' C' B' C'); Col.
      intro.
      subst C'.
      apply H19.
      Col.
    subst C''.
    contradiction.
Qed.

Lemma l13_18_3 : A B C A' B' C', ¬Col A B C
                                Par_strict A B A' B'
                                Par_strict A C A' C'
                                (Par_strict B C B' C' Par A A' B B')
                                (Par C C' A A' Par C C' B B').
Proof.
    intros.
    spliter.
    assert(Par C C' A A').
      apply par_distincts in H3.
      spliter.
      assert(HH:= parallel_existence1 B B' C H5).
      ex_and HH P.
      induction(Par_dec C P B C).
        induction H7.
          apply False_ind.
          apply H7.
           C.
          split; Col.
        spliter.
        assert(Col P B' C).
          induction H6.
            apply False_ind.
            apply H6.
             B.
            split; Col.
          spliter.
          Col.
        assert(Col C B B').
          apply (col_transitivity_1 _ P); Col.
        apply False_ind.
        apply H2.
         B'.
        split; Col.
      assert(¬ Par C P B' C').
        intro.
        apply H7.
        apply(par_trans _ _ B' C'); Par.
      assert(HH:=not_par_inter_exists C P B' C' H8).
      ex_and HH C''.
      induction(eq_dec_points B' C'').
        subst C''.
        apply False_ind.
        induction H6.
          apply H6.
           B'.
          split; Col.
        spliter; apply H2.
         B'.
        split; Col.
        apply col_permutation_1.
        apply(col_transitivity_1 _ P); Col.
      assert(Par C C'' B B' ).
        apply (par_col_par_2 _ P); Col.
          intro.
          subst C''.
          apply H2.
           C.
          split; Col.
        Par.
      assert(Par B' C'' B C).
        apply (par_col_par_2 _ C'); Col.
        left.
        Par.
      assert(¬ Col A' B' C').
        intro.
        apply H.
        assert(Par C' A' B C).
          apply (par_col_par_2 _ B').
            intro.
            subst C'.
            unfold Par_strict in H1.
            tauto.
            Col.
          apply par_left_comm.
          left.
          Par.
        assert(Par B C A C).
          apply (par_trans _ _ A' C'); Par.
        induction H16.
          apply False_ind.
          apply H16.
           C.
          split; Col.
        spliter; Col.
      assert(Par A C A' C'').
        apply(l13_15_par B A C B' A' C'').
          intro.
          apply H.
          Col.
          apply par_strict_comm.
          Par.
          induction H13.
            Par.
          spliter.
          apply False_ind.
          apply H2.
           B'.
          split; Col.
          Par.
        Par.
      assert(C' = C'').
        apply (l6_21 C' A' B' C'); Col.
          intro.
          subst C'.
          apply H14.
          Col.
          eapply (col_par_par_col A C A); Col.
            apply par_right_comm.
            left.
            Par.
          Par.
      subst C''.
      apply (par_trans _ _ B B'); Par.
    split.
      Par.
    apply (par_trans _ _ A A'); Par.
Qed.

Lemma l13_18 : A B C A' B' C' O, ¬Col A B C Par_strict A B A' B' Par_strict A C A' C'
                                        (Par_strict B C B' C' Col O A A' Col O B B' Col O C C')
                                           ((Par_strict B C B' C' Par A A' B B') (Par C C' A A' Par C C' B B'))
                                           (Par A A' B B' Par A A' C C' Par B C B' C').
Proof.
    intros.
    spliter.
    split.
      intros.
      apply (l13_18_2 A B C A' B' C' O); auto.
    split.
      intros.
      spliter.
      apply l13_18_3; auto.
    intros.
    spliter.
    apply (l13_15_par A B C A' B' C'); auto.
Qed.

Lemma l13_19_aux : A B C D A' B' C' D' O, ¬Col O A B A A' A C
                                           O A O A' O C O C'
                                           O B O B' O D O D'
                                           Col O A C Col O A A' Col O A C'
                                           Col O B D Col O B B' Col O B D'
                                           ¬Par A B C D
                                           Par A B A' B' Par A D A' D' Par B C B' C'
                                           Par C D C' D'.
Proof.
    intros.
    assert(HH:= not_par_inter_exists A B C D H16).
    ex_and HH E.
    assert(¬Par A' B' O E).
      intro.
      assert(Par A B O E).
        apply (par_trans _ _ A' B'); Par.
      induction H23.
        apply H23.
         E.
        split; Col.
      spliter.
      apply H.
      apply (col_transitivity_1 _ E); Col.
    assert(HH:= not_par_inter_exists A' B' O E H22).
    ex_and HH E'.
    assert(C E).
      intro.
      subst E.
      apply H.
      apply col_permutation_2.
      apply (col_transitivity_1 _ C); Col.
    induction(Col_dec A D E).
      assert(B = D).
        apply(l6_21 O B A E); Col.
        intro.
        subst E.
        apply H.
        assert(Col A O D).
          apply (col_transitivity_1 _ C); Col.
        apply (col_transitivity_1 _ D); Col.
      subst D.
      assert(Par A' B' A' D').
        apply (par_trans _ _ A B); Par.
      induction H27.
        apply False_ind.
        apply H27.
         A'.
        split; Col.
      spliter.
      assert(B' = D').
        eapply(l6_21 A' B' O B'); Col.
        intro.
        apply H.
        apply (col_transitivity_1 _ A'); Col.
        apply (col_transitivity_1 _ B'); Col.
        apply (col_transitivity_1 _ B); Col.
      subst D'.
      Par.
    assert(B B').
      intro.
      subst B'.
      induction H17.
        apply H17.
         B.
        split; Col.
      spliter.
      apply H.
      apply col_permutation_2.
      apply (col_transitivity_1 _ A'); Col.
    assert(Par D E D' E').
      eapply (l13_15 A _ _ A' _ _ O); Col.
        induction H18.
          auto.
        spliter.
        apply False_ind.
        assert(Col A' A D).
          apply (col_transitivity_1 _ D'); Col.
        assert(Col A O D).
          apply (col_transitivity_1 _ A'); Col.
        apply H.
        apply (col_transitivity_1 _ D); Col.
        assert(Par A E A' E').
          apply(par_col_par_2 _ B); Col.
            intro.
            subst E.
            apply H26.
            Col.
          apply par_symmetry.
          apply(par_col_par_2 _ B'); Col.
            intro.
            subst E'.
            assert(Col O A E).
              apply(col_transitivity_1 _ A'); Col.
            apply H.
            apply col_permutation_2.
            apply(col_transitivity_1 _ E); Col.
            intro.
            subst E.
            apply H26.
            Col.
          Par.
        induction H28.
          auto.
        spliter.
        apply False_ind.
        assert(Col A' A E).
          apply(col_transitivity_1 _ E'); Col.
        assert(Col A O E).
          apply(col_transitivity_1 _ A'); Col.
        apply H.
        apply col_permutation_2.
        apply(col_transitivity_1 _ E); Col.
      apply(col_transitivity_1 _ B); Col.
    apply par_comm.
    induction(Col_dec B C E).
      assert(B = D).
        apply(l6_21 O B C E); Col.
        intro.
        apply H.
        apply (col_transitivity_1 _ C); Col.
      subst D.
      assert(Par A' B' A' D').
        apply (par_trans _ _ A B); Par.
      induction H30.
        apply False_ind.
        apply H30.
         A'.
        split; Col.
      spliter.
      assert(B' = D').
        eapply(l6_21 A' B' O B'); Col.
          Col5.
        ColR.
      subst D'.
      Par.
    assert(Par C E C' E').
      eapply (l13_15 B _ _ B' _ _ O); Col.
        induction H19.
          auto.
        spliter.
        apply False_ind.
        apply H.
        assert(Col B O C').
          apply (col_transitivity_1 _ B'); Col.
        apply (col_transitivity_1 _ C'); Col.
        assert(Par B E B' E').
          apply (par_col_par_2 _ A); Col.
            intro.
            subst E.
            apply H29.
            Col.
          apply par_symmetry.
          apply (par_col_par_2 _ A'); Col.
            intro.
            subst E'.
            assert(Col O B E).
              apply (col_transitivity_1 _ B'); Col.
            apply H.
            apply col_permutation_1.
            apply (col_transitivity_1 _ E); Col.
            intro.
            subst E.
            apply H29.
            Col.
          Par.
        induction H30.
          auto.
        spliter.
        apply False_ind.
        apply H.
        assert(Col O B' E').
          apply col_permutation_2.
          apply (col_transitivity_1 _ B); Col.
        assert(Col B' A' O).
          apply (col_transitivity_1 _ E'); Col.
        apply (col_transitivity_1 _ A'); Col.
        apply (col_transitivity_1 _ B'); Col.
      apply (col_transitivity_1 _ A); Col.
    apply(par_col_par_2 _ E); Col.
      intro.
      subst D.
      apply H.
      apply(col_transitivity_1 _ C); Col.
    apply par_symmetry.
    apply(par_col_par_2 _ E'); Col.
      intro.
      subst D'.
      apply H.
      apply(col_transitivity_1 _ C'); Col.
      apply (col_par_par_col D E C); Par.
      Col.
    Par.
Qed.

Lemma l13_19 : A B C D A' B' C' D' O, ¬Col O A B
                                           O A O A' O C O C'
                                           O B O B' O D O D'
                                           Col O A C Col O A A' Col O A C'
                                           Col O B D Col O B B' Col O B D'
                                           Par A B A' B' Par A D A' D' Par B C B' C'
                                           Par C D C' D'.
Proof.
    intros.
    induction (eq_dec_points A A').
      subst A'.
      assert(B = B').
        apply(l6_21 A B O B); Col.
        induction H14.
          apply False_ind.
          apply H14.
           A.
          split; Col.
        spliter.
        Col.
      subst B'.
      assert(D = D').
        apply(l6_21 A D O B); Col.
          intro.
          apply H.
          apply (col_transitivity_1 _ D); Col.
          induction H15.
            apply False_ind.
            apply H15.
             A.
            split; Col.
          spliter.
          Col.
      subst D'.
      assert(C = C').
        apply(l6_21 B C O A); Col.
          intro.
          apply H.
          apply (col_transitivity_1 _ C); Col.
          induction H16.
            apply False_ind.
            apply H16.
             B.
            split; Col.
          spliter.
          Col.
      subst C'.
      apply par_reflexivity.
      intro.
      subst D.
      apply H.
      apply (col_transitivity_1 _ C); Col.
    induction(eq_dec_points A C).
      subst C.
      assert(A' = C').
        assert(Par A' B' B' C').
          apply (par_trans _ _ A B); Par.
        induction H18.
          apply False_ind.
          apply H18.
           B'.
          split; Col.
        spliter.
        eapply (l6_21 B' C' O A); Col.
        intro.
        apply H.
        apply (col_transitivity_1 _ B'); Col.
        apply (col_transitivity_1 _ C'); Col.
      subst C'.
      auto.
    induction(eq_dec_points A' C').
      subst C'.
      assert(A = C).
        assert(Par A B B C).
          apply (par_trans _ _ A' B'); Par.
        induction H19.
          apply False_ind.
          apply H19.
           B.
          split; Col.
        spliter.
        eapply (l6_21 B C O A'); Col.
          intro.
          apply H.
          apply (col_transitivity_1 _ C); Col.
          apply (col_transitivity_1 _ A); Col.
      contradiction.
    induction(Par_dec C D C' D').
      auto.
    assert(HH:=not_par_one_not_par C D C' D' A' B' H20).
    induction HH.
      assert(¬ Par C D A B).
        intro.
        apply H21.
        apply (par_trans _ _ A B); Par.
      apply (l13_19_aux A B C D A' B' C' D' O); Col.
      intro.
      apply H21.
      apply (par_trans _ _ A B); Par.
    apply par_symmetry.
    apply (l13_19_aux A' B' C' D' A B C D O); Par.
      intro.
      apply H.
      apply (col_transitivity_1 _ A'); Col.
      apply (col_transitivity_1 _ B'); Col.
      apply (col_transitivity_1 _ A); Col.
      Col.
      apply (col_transitivity_1 _ A); Col.
      apply (col_transitivity_1 _ B); Col.
      Col.
    apply (col_transitivity_1 _ B); Col.
Qed.

Lemma l13_19_par_aux : A B C D A' B' C' D' X Y,
                                             X A X A' X C X C'
                                           Y B Y B' Y D Y D'
                                           Col X A C Col X A A' Col X A C'
                                           Col Y B D Col Y B B' Col Y B D'
                                           A C B D A A'
                                           Par_strict X A Y B
                                           ¬Par A B C D
                                           Par A B A' B' Par A D A' D' Par B C B' C'
                                           Par C D C' D'.
Proof.
    intros.
    assert(HH := not_par_inter_exists A B C D H17).
    ex_and HH E.
    assert(HH:= parallel_existence1 X A E H).
    ex_and HH Z.
    assert(¬Par A B E Z).
      intro.
      assert(Par Y B E Z).
        apply (par_trans _ _ X A); Par.
      induction H24.
        apply H24.
         E.
        split; Col.
      spliter.
      induction H23.
        apply H23.
         A.
        split; Col.
      spliter.
      induction H25.
        apply H25.
         B.
        split; Col.
      spliter.
      apply H16.
       E.
      split;ColR.
    assert(¬Par A' B' E Z).
      intro.
      apply H24.
      apply (par_trans _ _ A' B'); Par.
    assert(HH:= not_par_inter_exists A' B' E Z H25).
    ex_and HH E'.
    assert(¬Col A D E).
      intro.
      induction (eq_dec_points A E).
        subst E.
        apply H13.
        apply (l6_21 X A D A); Col.
          intro.
          apply H16.
           D.
          split; Col.
        apply par_distincts in H19.
        spliter.
        auto.
      assert(Col A B D) by ColR.
      apply H16.
       A.
      split; Col.
      ColR.
    assert(Par_strict X A E Z).
      induction H23.
        Par.
      spliter.
      apply False_ind.
      assert(Col E X A) by ColR.
      assert(Col A C E) by ColR.
      apply H13.
      apply (l6_21 A E D C); Col.
        intro.
        subst D.
        contradiction.
        apply col_permutation_2.
        apply (col_transitivity_1 _ E); Col.
        intro.
        subst E.
        clean_trivial_hyps.
        apply H16.
         B.
        split; Col.
        apply col_permutation_1.
        apply (col_transitivity_1 _ C); Col.
    assert(Par Y B E Z).
      apply (par_trans _ _ X A); Par.
    assert(Par_strict Y B E Z).
      induction H30.
        Par.
      spliter.
      apply False_ind.
      assert(Col E Y B) by ColR.
      assert(Col B D E) by ColR.
      apply H14.
      apply (l6_21 B E C D); Col.
        intro.
        apply H16.
         C.
        split; Col.
        apply col_permutation_1.
        apply (col_transitivity_1 _ E); Col.
        intro.
        subst E.
        apply H16.
         C.
        split; Col.
        clean_trivial_hyps.
        apply col_permutation_1.
        apply (col_transitivity_1 _ D); Col.
      intro.
      subst D.
      apply H16.
       C.
      split; Col.
      assert_diffs; ColR.
    assert(¬Col A' D' E').
      intro.
      assert(Col A' B' D').
        apply (col_transitivity_1 _ E'); Col.
        intro.
        subst E'.
        apply H29.
         A'.
        split; Col.
      apply H16.
       A'.
      split; Col.
      assert(Col Y B' D').
        apply (col_transitivity_1 _ B); Col.
      assert(Col B' A' Y).
        apply (col_transitivity_1 _ D'); Col.
        intro.
        subst D'.
        assert(Par A D A B).
          apply(par_trans _ _ A' B'); Par.
        induction H35.
          apply H35.
           A.
          split; Col.
        spliter.
        apply H16.
         A.
        split; Col.
        apply col_permutation_1.
        apply (col_transitivity_1 _ D); Col.
      apply col_permutation_2.
      apply (col_transitivity_1 _ B'); Col.
    assert(¬ Col X A B).
      intro.
      apply H16.
       B.
      split; Col.
    assert(¬ Col Y A B).
      intro.
      apply H16.
       A.
      split; Col.
    assert(B B').
      intro.
      subst B'.
      apply H15.
      apply(l6_21 X A B A); Col.
        intro.
        subst B.
        apply H33.
        Col.
        induction H18.
          apply False_ind.
          apply H18.
           B.
          split; Col.
        spliter.
        Col.
    assert(C C').
      intro.
      subst C'.
      induction H20.
        apply H20.
         C.
        split; Col.
      spliter.
      apply H16.
       C.
      split; Col.
      apply col_permutation_1.
      apply (col_transitivity_1 _ B'); Col.
    assert(D D').
      intro.
      subst D'.
      induction H19.
        apply H19.
         D.
        split; Col.
      spliter.
      apply H16.
       D.
      split; Col.
      apply col_permutation_1.
      apply (col_transitivity_1 _ A'); Col.
    assert(A' C').
      intro.
      subst C'.
      assert(Par B C A B).
        apply (par_trans _ _ A' B'); Par.
      induction H38.
        apply H38.
         B.
        split; Col.
      spliter.
      apply H16.
       B.
      split; ColR.
    assert(B' D').
      intro.
      subst D'.
      assert(Par A D A B).
        apply (par_trans _ _ A' B'); Par.
      induction H39.
        apply H39.
         A.
        split; Col.
      spliter.
      apply H16.
       A.
      split; Col.
      apply col_permutation_1.
      apply (col_transitivity_1 _ D); Col.
    assert(A E).
      intro.
      subst E.
      apply H28.
      Col.
    assert(A' E').
      intro.
      subst E'.
      apply H32.
      Col.
    assert(B E).
      intro.
      subst E.
      apply H31.
       B.
      split; Col.
    assert(B' E').
      intro.
      subst E'.
      apply H31.
       B'.
      split; Col.
    assert(Par A E A' E').
      apply (par_col_par_2 _ B); Col.
      apply par_symmetry.
      apply (par_col_par_2 _ B'); Col.
      Par.
    assert(Par_strict A E A' E').
      induction H44.
        Par.
      spliter.
      apply False_ind.
      apply H45.
      apply (l6_21 X A' B' E'); Col.
        intro.
        apply H16.
         B'.
        split; Col.
        apply col_permutation_2.
        apply (col_transitivity_1 _ A'); Col.
      apply col_permutation_2.
      apply (col_transitivity_1 _ A); Col.
    assert(Par D E D' E').
      apply(l13_15_par A D E A' D' E'); Par.
        induction H19.
          Par.
        spliter.
        apply False_ind.
        apply H16.
         D.
        split; Col.
        apply col_permutation_1.
        apply (col_transitivity_1 _ A'); Col.
        apply col_permutation_2.
        apply (col_transitivity_1 _ D'); Col.
        apply (par_col_par_2 _ X); Col.
        apply par_symmetry.
        apply (par_col_par_2 _ Y); Col.
          apply col_permutation_2.
          apply (col_transitivity_1 _ B); Col.
        apply par_comm.
        apply (par_col_par_2 _ B); Col.
        apply (par_trans _ _ E Z); Par.
      apply (par_col_par_2 _ X); Par; Col.
      apply par_symmetry.
      apply (par_col_par_2 _ Z); Col.
        intro.
        subst E'.
        apply H45.
         E.
        split; Col.
      Par.
    assert(Par C E C' E').
      eapply(l13_15_par B C E B' C' E'); Par.
        intro.
        assert(Col B A C) by ColR.
        apply H16.
         B.
        split; ColR.
        induction H20.
          Par.
        spliter.
        apply False_ind.
        apply H16.
         B'.
        split; Col.
        assert(Col X C C').
          apply (col_transitivity_1 _ A); Col.
        assert(Col C B' X).
          apply (col_transitivity_1 _ C'); Col.
        apply col_permutation_2.
        apply (col_transitivity_1 _ C); Col.
        assert(Par B E B' E').
          apply (par_col_par_2 _ A); Col.
          apply par_symmetry.
          apply (par_col_par_2 _ A'); Col.
          Par.
        induction H47.
          Par.
        spliter.
        apply False_ind.
        assert(Col B' A' B) by ColR.
        apply H16.
         A'.
        split; sfinish.
        apply (par_col_par_2 _ Y); Col.
        apply par_symmetry.
        apply (par_col_par_2 _ X); Col.
          apply col_permutation_2.
          apply (col_transitivity_1 _ A); Col.
        apply par_left_comm.
        apply (par_col_par_2 _ A); Col.
        apply (par_trans _ _ E Z); Par.
      apply (par_col_par_2 _ Y); Col.
      apply par_symmetry.
      apply (par_col_par_2 _ Z); Col.
        intro.
        subst E'.
        apply H45.
         E.
        split; Col.
      Par.
    apply (par_col_par_2 _ E); Col.
      intro.
      subst D.
      apply H16.
       C.
      split; Col.
    apply par_symmetry.
    apply (par_col_par_2 _ E'); Col.
      intro.
      subst D'.
      apply H16.
       C'.
      split; Col.
      apply (col_par_par_col C E D); Col ; Par.
    Par.
Qed.

Lemma l13_19_par : A B C D A' B' C' D' X Y,
 X A X A' X C X C' Y B Y B' Y D Y D'
 Col X A C Col X A A' Col X A C' Col Y B D Col Y B B' Col Y B D'
 Par_strict X A Y B Par A B A' B' Par A D A' D' Par B C B' C'
 Par C D C' D'.
Proof.
    intros.
    induction(eq_dec_points A C).
      subst C.
      assert(Par A' B' B' C').
        apply(par_trans _ _ A B); Par.
      induction H17.
        apply False_ind.
        apply H17.
         B'.
        split; Col.
      spliter.
      assert(A' = C').
        apply (l6_21 X A B' A'); Col.
        intro.
        apply H13.
         B'.
        split; Col.
      subst C'.
      Par.
    induction(eq_dec_points B D).
      subst D.
      assert(Par A' B' A' D').
        apply(par_trans _ _ A B); Par.
      induction H18.
        apply False_ind.
        apply H18.
         A'.
        split; Col.
      spliter.
      assert(B' = D').
        apply (l6_21 Y B A' B'); Col.
        intro.
        apply H13.
         A'.
        split; Col.
      subst D'.
      Par.
    induction(eq_dec_points A A').
      subst A'.
      induction H14.
        apply False_ind.
        apply H14.
         A.
        split; Col.
      spliter.
      assert(B = B').
        apply (l6_21 Y B A B); Col.
        intro.
        apply H13.
         A.
        split; Col.
      subst B'.
      assert(C = C').
        induction H16.
          apply False_ind.
          apply H16.
           B.
          split; Col.
        spliter.
        apply (l6_21 X A B C); Col.
        intro.
        apply H13.
         B.
        split; Col.
      subst C'.
      assert(D = D').
        induction H15.
          apply False_ind.
          apply H15.
           A.
          split; Col.
        spliter.
        apply (l6_21 Y B A D); Col.
        intro.
        apply H13.
         A.
        split; Col.
      subst D'.
      auto.
      apply par_reflexivity.
      intro.
      subst D.
      clean_trivial_hyps.
      apply H13.
       C.
      split; Col.
    induction(Par_dec C D C' D').
      auto.
    assert(HH:=not_par_one_not_par C D C' D' A B H20).
    induction HH.
      eapply (l13_19_par_aux A B C D A' B' C' D' X Y); Col.
      intro.
      apply H21.
      Par.
    apply par_distincts in H14.
    spliter.
    apply par_symmetry.
    eapply (l13_19_par_aux A' B' C' D' A B C D X Y); sfinish.
      intro.
      subst C'.
      apply H17.
      apply (l6_21 X A B A); finish.
        intro.
        apply H13.
         B.
        split; Col.
        assert(Par B C B A).
          apply(par_trans _ _ A' B');finish.
        induction H24.
          apply False_ind.
          apply H24.
           B.
          split; Col.
        spliter.
        Col.
      intro.
      apply H18.
      subst D'.
      assert(Par A D A B).
        apply(par_trans _ _ A' B'); Par.
      apply (l6_21 Y B A B); Col.
        intro.
        apply H13.
         A.
        split; Col.
        induction H24.
          apply False_ind.
          apply H24.
           A.
          split; Col.
        spliter.
        Col.
      unfold Par_strict in H13.
      spliter.
      unfold Par_strict.
      repeat split; auto; try apply all_coplanar.
      intro.
      apply H26.
      ex_and H27 P.
       P.
      split.
        ColR.
      ColR.
    intro.
    apply H21.
    apply (par_trans _ _ A' B'); Par.
Qed.

End Desargues_Hessenberg.