Library GeoCoq.Tarski_dev.Ch14_sum

Require Export GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg.

Section T14_sum.

Context `{TE:Tarski_2D_euclidean}.

Lemma Pj_exists : ∀ A B C,
 ∃ D, Pj A B C D.
Proof.
    intros.
    unfold Pj in ×.
    elim (eq_dec_points A B);intro.
      subst.
      ∃ C.
      tauto.
    assert (T:=parallel_existence A B C H).
    decompose [and ex] T;clear T.
    ∃ x0.
    induction (eq_dec_points C x0).
      tauto.
    eauto using par_col2_par with col.
Qed.

Lemma sum_to_sump : ∀ O E E' A B C, Sum O E E' A B C → Sump O E E' A B C.
Proof.
    intros.
    unfold Sum in H.
    unfold Ar2 in H.
    spliter.
    repeat split; Col.
    ex_and H0 A'.
    ex_and H4 C'.
    ∃ A'.
    ∃ C'.
    assert(O ≠ E ∧ O ≠ E').
      repeat split; intro; subst O; apply H; Col.
    spliter.
    assert(HH:=parallel_existence1 O E A' H8).
    ex_and HH P'.
    ∃ P'.
    assert( E ≠ E').
      intro.
      subst E'.
      apply H.
      Col.
    repeat split; Col.
      intro.
      induction H12.
        apply H12.
        ∃ E'.
        split; Col.
      spliter.
      contradiction.
      unfold Pj in H0.
      induction H0.
        left.
        apply par_symmetry.
        assumption.
      right.
      auto.
      apply par_distincts in H10.
      spliter.
      auto.
      intro.
      assert(Par O E O E').
        apply (par_trans _ _ A' P'); auto.
      induction H13.
        apply H13.
        ∃ O.
        split; Col.
      spliter.
      apply H.
      Col.
      unfold Pj in H5.
      induction H5.
        assert(Par A' C' A' P').
          apply (par_trans _ _ O E).
            apply par_symmetry.
            auto.
          auto.
        induction H12.
          apply False_ind.
          apply H12.
          ∃ A'.
          split; Col.
        spliter.
        Col.
      subst C'.
      Col.
      unfold Pj in H6.
      induction H6.
        left.
        apply par_symmetry.
        auto.
      right.
      auto.
      intro.
      induction H12.
        apply H12.
        ∃ E.
        split; Col.
      spliter.
      contradiction.
    unfold Pj in H7.
    induction H7.
      left.
      apply par_symmetry.
      apply par_left_comm.
      auto.
    tauto.
Qed.

Lemma sump_to_sum : ∀ O E E' A B C, Sump O E E' A B C → Sum O E E' A B C.
Proof.
    intros.
    unfold Sump in H.
    spliter.
    ex_and H1 A'.
    ex_and H2 C'.
    ex_and H1 P'.
    unfold Sum.
    split.
      repeat split; Col.
        intro.
        unfold Proj in H1.
        spliter.
        apply H7.
        right.
        repeat split; Col.
      unfold Proj in H4.
      spliter.
      Col.
    ∃ A'.
    ∃ C'.
    unfold Pj.
    repeat split.
      unfold Proj in H1.
      spliter.
      induction H8.
        left.
        apply par_symmetry.
        auto.
      tauto.
      unfold Proj in H1.
      tauto.
      induction(eq_dec_points A' C').
        tauto.
      left.
      unfold Proj in H3.
      spliter.
      apply (par_col_par _ _ _ P'); Col.
      unfold Proj in H3.
      spliter.
      induction H8.
        left.
        apply par_symmetry.
        auto.
      tauto.
    unfold Proj in H4.
    spliter.
    induction H8.
      left.
      apply par_symmetry.
      apply par_right_comm.
      auto.
    tauto.
Qed.


Lemma project_col_project : ∀ A B C P P' X Y,
  A ≠ C → Col A B C →
  Proj P P' A B X Y →
  Proj P P' A C X Y.
Proof with finish.
    intros.
    unfold Proj in ×.
    spliter.
    repeat split; auto.
      intro.
      apply H3.
      eapply (par_col_par_2 _ C); Col; Par.
    ColR.
Qed.

Lemma project_trivial : ∀ P A B X Y,
  A ≠ B → X ≠ Y →
  Col A B P → ¬ Par A B X Y →
  Proj P P A B X Y.
Proof.
    intros.
    unfold Proj.
    repeat split; Col.
Qed.

Lemma pj_col_project : ∀ P P' A B X Y,
 A ≠ B → X ≠ Y →
 Col P' A B →
 ¬ Par A B X Y →
 Pj X Y P P' →
 Proj P P' A B X Y.
Proof.
    intros.
    unfold Pj in H3.
    induction H3.
      unfold Proj.
      repeat split; Col.
      left.
      apply par_symmetry.
      assumption.
    subst P'.
    apply project_trivial; Col.
Qed.

Section Grid.

Variable O E E' : Tpoint.

Variable grid_ok : ¬ Col O E E'.

Lemma sum_exists : ∀ A B,
 Col O E A → Col O E B →
 ∃ C, Sum O E E' A B C.
Proof.
    intros.
    assert(NC:= grid_ok).
    assert(O ≠ E).
      intro.
      subst E.
      apply NC.
      Col.
    assert(O ≠ E').
      intro.
      subst E'.
      apply NC.
      Col.
    induction(eq_dec_points O A).
      subst A.
      ∃ B.
      unfold Sum.
      split.
        unfold Ar2.
        split; Col.
      ∃ O.
      ∃ B.
      unfold Pj.
      repeat split.
        right.
        auto.
        Col.
        induction(eq_dec_points O B).
          right; auto.
        left.
        right.
        repeat split; Col.
        right; auto.
      right; auto.
    assert(∃! A' , Proj A A' O E' E E').
      apply(project_existence A O E' E E'); intro; try (subst E' ; apply NC; Col).
      induction H4.
        apply H4.
        ∃ E'.
        split; Col.
      spliter.
      apply NC.
      Col.
    ex_and H4 A'.
    assert(HH:=parallel_existence1 O E A' H1).
    ex_and HH P.
    unfold unique in H5.
    spliter.
    assert(A ≠ A').
      intro.
      subst A'.
      apply project_col in H5.
      apply NC.
      apply (col_transitivity_1 _ A); Col.
    induction(eq_dec_points B O).
      subst B.
      ∃ A.
      unfold Sum.
      split.
        unfold Ar2.
        repeat split; Col.
      ∃ A'.
      ∃ A'.
      unfold Pj.
      unfold Proj in H5.
      spliter.
      repeat split.
        spliter.
        induction H11.
          left.
          apply par_symmetry.
          auto.
        contradiction.
        Col.
        right.
        auto.
        left.
        right.
        repeat split; Col.
        intro.
        subst A'.
        induction H11.
          induction H11.
            apply H11.
            ∃ E.
            split; Col.
          spliter.
          contradiction.
        contradiction.
      induction H11.
        left.
        apply par_symmetry.
        apply par_comm.
        auto.
      contradiction.
    assert(∃! C', Proj B C' A' P O E').
      apply(project_existence B A' P O E'); auto.
      apply par_distincts in H4.
      spliter.
      auto.
      intro.
      assert(Par O E O E').
        apply (par_trans _ _ A' P).
          auto.
        apply par_symmetry.
        auto.
      induction H10.
        apply H10.
        ∃ O.
        split; Col.
      spliter.
      apply NC.
      Col.
    ex_and H9 C'.
    unfold unique in H10.
    spliter.
    assert(∃! C : Tpoint, Proj C' C O E A A').
      apply(project_existence C' O E A A'); auto.
      intro.
      induction H11.
        apply H11.
        ∃ A.
        split; Col.
      spliter.
      assert(HH:=project_par_dir A A' O E' E E' H11 H5).
      assert(Col E A A').
        ColR.
      induction HH.
        apply H16.
        ∃ E.
        split; Col.
      spliter.
      apply NC.
      apply col_permutation_2.
      apply(col_transitivity_1 _ A'); Col.
      intro.
      subst A'.
      clean_trivial_hyps.
      unfold Proj in H5.
      spliter.
      apply NC.
      Col.
    ex_and H11 C.
    unfold unique in H12.
    spliter.
    unfold Proj in ×.
    spliter.
    ∃ C.
    unfold Sum.
    split.
      unfold Ar2.
      repeat split; Col.
    ∃ A'.
    ∃ C'.
    unfold Pj.
    repeat split.
      left.
      induction H24.
        apply par_symmetry.
        auto.
      contradiction.
      Col.
      left.
      eapply (par_col_par _ _ _ P).
        intro.
        subst C'.
        induction H16.
          induction H16.
            apply H16.
            ∃ A'.
            split; Col.
          spliter.
          induction H20.
            induction H20.
              apply H20.
              ∃ A'.
              split; Col.
            spliter.
            apply NC.
            apply (col_transitivity_1 _ B); Col.
          subst A'.
          apply H14.
          right.
          repeat split; try finish; ColR.
        subst A'.
        apply H14.
        right.
        repeat split; try finish; ColR.
        assumption.
      ColR.
      induction H20.
        left.
        apply par_symmetry.
        auto.
      right; auto.
    induction H24.
      induction H16.
        left.
        apply (par_trans _ _ A A').
          apply par_symmetry.
          apply par_right_comm.
          auto.
        apply par_symmetry.
        auto.
      subst C'.
      right.
      auto.
    contradiction.
Qed.

Lemma sum_uniqueness : ∀ A B C1 C2,
 Sum O E E' A B C1 →
 Sum O E E' A B C2 →
 C1 = C2.
Proof.
    intros.
    apply sum_to_sump in H.
    apply sum_to_sump in H0.
    unfold Sump in H.
    unfold Sump in H0.
    spliter.
    clean_duplicated_hyps.
    ex_and H4 A'.
    ex_and H0 C'.
    ex_and H1 P'.
    ex_and H2 A''.
    ex_and H6 C''.
    ex_and H2 P''.
    assert(A'=A'').
      apply(project_uniqueness A A' A'' O E' E E');auto.
    subst A''.
    assert(Col A' P' P'').
      assert(Par A' P' A' P'').
        apply (par_trans _ _ O E).
          apply par_symmetry.
          auto.
        auto.
      induction H9.
        apply False_ind.
        apply H9.
        ∃ A'.
        split; Col.
      spliter.
      Col.
    assert(Proj B C'' A' P' O E').
      eapply (project_col_project _ P''); Col.
      unfold Proj in H4.
      tauto.
    assert(C' = C'').
      apply(project_uniqueness B C' C'' A' P' O E');auto.
    subst C''.
    apply(project_uniqueness C' C1 C2 O E E E');auto.
Qed.

Lemma opp_exists : ∀ A,
 Col O E A →
 ∃ MA, Opp O E E' A MA.
Proof.
    intros.
    assert(NC:= grid_ok).
    induction(eq_dec_points A O).
      subst A.
      ∃ O.
      unfold Opp.
      unfold Sum.
      split.
        unfold Ar2.
        repeat split; Col.
      ∃ O.
      ∃ O.
      repeat split; Col; try right; auto.
    prolong A O MA A O.
    ∃ MA.
    unfold Opp.
    apply sump_to_sum.
    unfold Sump.
    repeat split.
      apply bet_col in H1.
      apply (col_transitivity_1 _ A);Col.
      Col.
    assert(E ≠ E' ∧ O ≠ E').
      split; intro; subst E'; apply NC; Col.
    spliter.
    assert(∃! P' : Tpoint, Proj MA P' O E' E E').
      apply(project_existence MA O E' E E'); auto.
      intro.
      induction H5.
        apply H5.
        ∃ E'.
        split; Col.
      spliter.
      apply NC.
      Col.
    ex_and H5 A'.
    unfold unique in H6.
    spliter.
    ∃ A'.
    assert(O ≠ E).
      intro.
      subst E.
      apply NC.
      Col.
    assert(HH:= parallel_existence1 O E A' H7).
    ex_and HH P'.
    assert(∃! C' : Tpoint, Proj A C' A' P' O E').
      apply(project_existence A A' P' O E'); auto.
      apply par_distincts in H8.
      spliter.
      auto.
      intro.
      assert(Par O E O E').
        apply (par_trans _ _ A' P').
          auto.
        apply par_symmetry; auto.
      induction H10.
        apply H10.
        ∃ O.
        split; Col.
      spliter.
      apply NC.
      Col.
    ex_and H9 C'.
    unfold unique in H10.
    spliter.
    ∃ C'.
    ∃ P'.
    split; auto.
    split; auto.
    split; auto.
    unfold Proj in H5.
    spliter.
    unfold Proj.
    repeat split; Col.
      intro.
      induction H15.
        apply H15.
        ∃ E.
        split; Col.
      apply NC.
      tauto.
    left.
    unfold Proj in H9.
    spliter.
    assert(Par O E' O A').
      right.
      repeat split; Col.
      intro.
      subst A'.
      clean_trivial_hyps.
      induction H14.
        induction H13.
          apply H13.
          ∃ E.
          split; Col.
          apply col_permutation_1.
          apply bet_col in H1.
          apply(col_transitivity_1 _ A); Col.
        apply NC.
        tauto.
      subst MA.
      apply cong_symmetry in H2.
      apply cong_identity in H2.
      contradiction.
    assert(Plg A C' A' O).
      apply pars_par_plg.
        induction H18.
          assert(Par A C' A' O).
            apply (par_trans _ _ O E').
              Par.
            Par.
          induction H20.
            auto.
          spliter.
          apply False_ind.
          apply NC.
          apply (col_transitivity_1 _ A'); Col.
          apply (col_transitivity_1 _ A); Col.
        subst C'.
        apply False_ind.
        induction H8.
          apply H8.
          ∃ A.
          split; Col.
        spliter.
        apply NC.
        apply (col_transitivity_1 _ A'); Col.
          intro.
          subst A'.
          apply par_distincts in H19.
          tauto.
        apply col_permutation_2.
        apply (col_transitivity_1 _ P'); Col.
      apply par_comm.
      apply (par_col_par _ _ _ P').
        intro.
        subst C'.
        induction H18.
          induction H18.
            apply H18.
            ∃ A'.
            split; Col.
          spliter.
          apply NC.
          apply (col_transitivity_1 _ A); Col.
        subst A'.
        induction H19.
          apply H18.
          ∃ O.
          split; Col.
        spliter.
        apply NC.
        apply (col_transitivity_1 _ A); Col.
        apply par_symmetry.
        apply (par_col_par _ _ _ E); Col.
        apply par_symmetry.
        Par.
      Col.
    assert(Parallelogram A O MA O).
      right.
      unfold Parallelogram_flat.
      repeat split; Col; Cong.
      left.
      intro.
      subst MA.
      apply between_identity in H1.
      contradiction.
    apply plg_to_parallelogram in H20.
    apply plg_permut in H20.
    apply plg_comm2 in H21.
    assert(Parallelogram C' A' MA O).
      assert(HH:= plg_pseudo_trans C' A' O A O MA H20 H21).
      induction HH.
        auto.
      spliter.
      subst MA.
      apply cong_symmetry in H2.
      apply cong_identity in H2.
      contradiction.
    apply plg_par in H22.
      spliter.
      induction H14.
        apply (par_trans _ _ A' MA).
          auto.
        Par.
      subst MA.
      apply par_distincts in H23.
      tauto.
      intro.
      subst C'.
      unfold Parallelogram in H20.
      induction H20.
        unfold Parallelogram_strict in H20.
        spliter.
        apply par_distincts in H23.
        tauto.
      unfold Parallelogram_flat in H20.
      spliter.
      apply cong_symmetry in H24.
      apply cong_identity in H24.
      subst A.
      tauto.
    intro.
    subst MA.
    unfold Parallelogram in H21.
    induction H21.
      unfold Parallelogram_strict in H21.
      spliter.
      unfold TS in H21; unfold Parallelogram.
      spliter; Col.
    unfold Parallelogram_flat in H21.
    spliter.
    apply NC.
    apply (col_transitivity_1 _ A); Col.
    apply (col_transitivity_1 _ A'); Col.
    intro.
    subst A'.
    apply cong_identity in H24.
    subst A.
    tauto.
Qed.

Lemma opp0 : Opp O E E' O O.
Proof.
    assert(NC:=grid_ok).
    assert(O ≠ E' ∧ E ≠ E').
      split; intro ; subst E'; apply NC; Col.
    spliter.
    assert(O ≠ E).
      intro.
      subst E.
      apply NC; Col.
    unfold Opp.
    apply sump_to_sum.
    unfold Sump.
    repeat split; Col.
    ∃ O.
    ∃ O.
    ∃ E.
    split.
      apply project_trivial; Col.
      intro.
      induction H2.
        apply H2.
        ∃ E'.
        split; Col.
      spliter.
      contradiction.
    split.
      apply par_reflexivity; auto.
    split.
      apply project_trivial; Col.
      intro.
      induction H2.
        apply H2.
        ∃ O.
        split; Col.
      spliter.
      apply NC.
      Col.
    apply project_trivial; Col.
    intro.
    induction H2.
      apply H2.
      ∃ E.
      split; Col.
    spliter.
    contradiction.
Qed.

Lemma pj_trivial : ∀ A B C, Pj A B C C.
Proof.
    intros.
    unfold Pj.
    right.
    auto.
Qed.

Lemma sum_O_O : Sum O E E' O O O.
Proof.
    unfold Sum.
    assert(O ≠ E' ∧ E ≠ E').
      split; intro ; subst E'; apply grid_ok; Col.
    split.
      spliter.
      unfold Ar2.
      repeat split; Col.
    ∃ O.
    ∃ O.
    repeat split;try (apply pj_trivial).
    Col.
Qed.

Lemma sum_A_O : ∀ A, Col O E A → Sum O E E' A O A.
Proof.
    intros.
    unfold Sum.
    split.
      repeat split; Col.
    assert(O ≠ E' ∧ E ≠ E').
      split; intro; subst E'; apply grid_ok; Col.
    spliter.
    induction (eq_dec_points A O).
      ∃ O.
      ∃ O.
      repeat split; Col; unfold Pj ; try auto.
    assert(¬ Par E E' O E').
      intro.
      induction H3.
        apply H3.
        ∃ E'.
        split; Col.
      spliter.
      apply grid_ok.
      Col.
    assert(HH:= project_existence A O E' E E' H1 H0 H3).
    ex_and HH A'.
    unfold unique in H4.
    spliter.
    ∃ A'.
    ∃ A'.
    unfold Proj in H4.
    spliter.
    repeat split; Col.
      unfold Pj.
      induction H9.
        left.
        apply par_symmetry.
        Par.
      tauto.
      unfold Pj.
      tauto.
      unfold Pj.
      left.
      right.
      repeat split; Col.
      intro.
      subst A'.
      induction H9.
        induction H9.
          apply H9.
          ∃ E.
          split; Col.
        spliter.
        contradiction.
      contradiction.
    unfold Pj.
    induction H9.
      left.
      apply par_symmetry.
      Par.
    right.
    auto.
Qed.

Lemma sum_O_B : ∀ B, Col O E B → Sum O E E' O B B.
Proof.
    intros.
    induction(eq_dec_points B O).
      subst B.
      apply sum_O_O.
    unfold Sum.
    split.
      repeat split; Col.
    assert(O ≠ E' ∧ E ≠ E').
      split; intro; subst E'; apply grid_ok; Col.
    spliter.
    assert(¬ Par E E' O E').
      intro.
      induction H3.
        apply H3.
        ∃ E'.
        split; Col.
      spliter.
      apply grid_ok.
      Col.
    ∃ O.
    ∃ B.
    repeat split; try(apply pj_trivial).
      Col.
    left.
    right.
    repeat split; Col.
    intro.
    subst E.
    apply grid_ok.
    Col.
Qed.

Lemma opp0_uniqueness : ∀ M, Opp O E E' O M → M = O.
Proof.
    intros.
    assert(NC:= grid_ok).
    unfold Opp in H.
    apply sum_to_sump in H.
    unfold Sump in H.
    spliter.
    ex_and H1 A'.
    ex_and H2 C'.
    ex_and H1 P'.
    unfold Proj in ×.
    spliter.
    induction H8.
      induction H12.
        assert(Par O E' E E').
          apply (par_trans _ _ C' O).
            apply par_symmetry.
            Par.
          Par.
        apply False_ind.
        induction H17.
          apply H17.
          ∃ E'.
          split; Col.
        spliter.
        contradiction.
      subst C'.
      apply par_distincts in H8.
      tauto.
    subst C'.
    assert( A' = O).
      apply (l6_21 O E E' O); Col.
      induction H2.
        apply False_ind.
        apply H2.
        ∃ O.
        split; Col.
      spliter.
      apply col_permutation_1.
      apply(col_transitivity_1 _ P'); Col.
    subst A'.
    induction H16.
      induction H8.
        apply False_ind.
        apply H8.
        ∃ E.
        split; Col.
      spliter.
      contradiction.
    assumption.
Qed.

Lemma proj_pars : ∀ A A' C' , A ≠ O → Col O E A → Par O E A' C' → Proj A A' O E' E E' → Par_strict O E A' C'.
Proof.
    intros.
    unfold Par_strict.
    assert(HH:=grid_ok).
    repeat split; try apply all_coplanar.
      intro.
      subst E.
      apply HH.
      Col.
      apply par_distincts in H1.
      tauto.
    intro.
    ex_and H3 X.
    unfold Proj in H2.
    spliter.
    induction H1.
      apply H1.
      ∃ X.
      split; Col.
    spliter.
    assert(Col A' O E).
      apply (col_transitivity_1 _ C'); Col.
    induction(eq_dec_points A' O).
      subst A'.
      clean_trivial_hyps.
      induction H8.
        induction H7.
          apply H7.
          ∃ E.
          split; Col.
        spliter.
        contradiction.
      contradiction.
    apply grid_ok.
    apply(col_transitivity_1 _ A'); Col.
Qed.

Lemma proj_col : ∀ A A' C' , A = O → Col O E A → Par O E A' C' → Proj A A' O E' E E' → A' = O.
Proof.
    intros.
    assert(HH:=grid_ok).
    unfold Proj in H2.
    spliter.
    subst A.
    induction H6.
      apply False_ind.
      apply H4.
      apply par_symmetry.
      eapply (par_col_par _ _ _ A'); Col.
      apply par_symmetry.
      Par.
    auto.
Qed.

Lemma grid_not_par : ¬Par O E E E' ∧ ¬Par O E O E' ∧ ¬Par O E' E E' ∧ O ≠ E ∧ O ≠ E' ∧ E ≠ E'.
Proof.
    repeat split.
      intro.
      unfold Par in H.
      induction H.
        apply H.
        ∃ E.
        split; Col.
      spliter.
      contradiction.
      intro.
      induction H.
        apply H.
        ∃ O.
        split; Col.
      spliter.
      apply grid_ok.
      Col.
      intro.
      induction H.
        apply H.
        ∃ E'.
        split; Col.
      spliter.
      contradiction.
      intro.
      subst E.
      apply grid_ok.
      Col.
      intro.
      subst E'.
      apply grid_ok.
      Col.
    intro.
    subst E'.
    apply grid_ok.
    Col.
Qed.

Lemma proj_id : ∀ A A', Proj A A' O E' E E' → Col O E A → Col O E A' → A = O.
Proof.
    intros.
    assert(HH:=grid_not_par).
    spliter.
    unfold Proj in H.
    spliter.
    induction H11.
      apply(l6_21 O E E' O); Col.
        assert(Col O A' A).
          apply(col_transitivity_1 _ E); Col.
        apply col_permutation_2.
        apply (col_transitivity_1 _ A'); Col.
        intro.
        subst A'.
        induction H11.
          apply H11.
          ∃ E.
          split; Col.
        spliter.
        contradiction.
    subst.
    apply(l6_21 O E E' O); Col.
Qed.

Lemma sum_O_B_eq : ∀ B C, Sum O E E' O B C → B = C.
Proof.
    intros.
    assert (HS:=H).
    unfold Sum in H.
    spliter.
    unfold Ar2 in H.
    spliter.
    assert(HH:=sum_O_B B H2).
    apply (sum_uniqueness O B); auto.
Qed.

Lemma sum_A_O_eq : ∀ A C, Sum O E E' A O C → A = C.
Proof.
    intros.
    assert (HS:=H).
    unfold Sum in H.
    spliter.
    unfold Ar2 in H.
    spliter.
    assert(HH:=sum_A_O A H1).
    apply (sum_uniqueness A O); auto.
Qed.

Lemma sum_par_strict : ∀ A B C A' C', Ar2 O E E' A B C → A ≠ O → Pj E E' A A' → Col O E' A' → Pj O E A' C' → Pj O E' B C' → Pj E' E C' C
                                           → A' ≠ O ∧ (Par_strict O E A' C' ∨ B = O).
Proof.
    intros.
    assert(Sum O E E' A B C).
      unfold Sum.
      split.
        auto.
      ∃ A'.
      ∃ C'.
      repeat split; auto.
    unfold Ar2 in H.
    unfold Pj in ×.
    spliter.
    assert(A' ≠ O).
      intro.
      subst A'.
      induction H3.
        induction H3.
          apply H3.
          ∃ O.
          split; Col.
        spliter.
        induction H1.
          induction H1.
            apply H1.
            ∃ E.
            split; Col.
          spliter.
          apply grid_ok.
          apply(col_transitivity_1 _ A); Col.
        contradiction.
      subst C'.
      induction H1.
        induction H1.
          apply H1.
          ∃ E.
          split; Col.
        spliter.
        apply grid_ok.
        apply(col_transitivity_1 _ A); Col.
      contradiction.
    split.
      auto.
    induction(eq_dec_points B O).
      tauto.
    left.
    induction H3.
      induction H3.
        assumption.
      spliter.
      apply False_ind.
      apply grid_ok.
      assert(Col A' O E ).
        apply(col_transitivity_1 _ C'); Col.
      apply(col_transitivity_1 _ A'); Col.
    subst C'.
    apply False_ind.
    induction H4.
      induction H3.
        apply H3.
        ∃ A'.
        split; Col.
      spliter.
      assert(Col O B E').
        apply (col_transitivity_1 _ A'); Col.
      apply grid_ok.
      apply (col_transitivity_1 _ B); Col.
    subst A'.
    assert(HH:= grid_not_par).
    spliter.
    induction H5.
      apply H3.
      apply par_symmetry.
      apply (par_col_par _ _ _ B); Col.
      apply par_right_comm.
      apply (par_col_par _ _ _ C); Par.
      apply col_permutation_1.
      apply(col_transitivity_1 _ E); Col.
    subst C.
    apply grid_ok.
    apply(col_transitivity_1 _ B); Col.
Qed.

Lemma sum_A_B_A : ∀ A B, Sum O E E' A B A → B = O.
Proof.
    intros.
    unfold Sum in H.
    spliter.
    ex_and H0 A'.
    ex_and H1 C'.
    assert(HH:= grid_not_par).
    spliter.
    induction(eq_dec_points A O).
      subst A.
      unfold Pj in ×.
      unfold Ar2 in H.
      spliter.
      induction H0.
        induction H0.
          apply False_ind.
          apply H0.
          ∃ E'.
          split; Col.
        spliter.
        apply False_ind.
        apply grid_ok.
        ColR.
      subst A'.
      induction H2.
        induction H4.
          apply False_ind.
          apply H5.
          apply (par_trans _ _ O C') ; Par.
        subst C'.
        apply par_distincts in H0.
        tauto.
      subst C'.
      induction H3.
        induction H0.
          apply False_ind.
          apply H0.
          ∃ O.
          split; Col.
        spliter.
        induction(eq_dec_points B O).
          auto.
        apply False_ind.
        apply grid_ok.
        ColR.
      assumption.
    assert(A' ≠ O ∧ (Par_strict O E A' C' ∨ B = O)).
      apply(sum_par_strict A B A A' C');auto.
    spliter.
    induction(eq_dec_points B O).
      auto.
    induction H13.
      unfold Pj in ×.
      unfold Ar2 in H.
      spliter.
      induction H0.
        induction H4.
          assert(Par A A' A C').
            apply (par_trans _ _ E E'); Par.
          apply False_ind.
          induction H18.
            apply H18.
            ∃ A.
            split; Col.
          spliter.
          apply H13.
          ∃ A.
          split; Col.
        subst C'.
        apply False_ind.
        apply H13.
        ∃ A.
        split; Col.
      subst A'.
      apply False_ind.
      apply grid_ok.
      apply(col_transitivity_1 _ A);Col.
    contradiction.
Qed.

Lemma sum_A_B_B : ∀ A B, Sum O E E' A B B → A = O.
Proof.
    intros.
    unfold Sum in H.
    spliter.
    ex_and H0 A'.
    ex_and H1 C'.
    assert(HH:= grid_not_par).
    spliter.
    unfold Pj in ×.
    unfold Ar2 in H.
    spliter.
    induction H3.
      induction H4.
        apply False_ind.
        apply H7.
        apply(par_trans _ _ B C'); Par.
      subst C'.
      apply par_distincts in H3.
      tauto.
    subst C'.
    induction(eq_dec_points A O).
      auto.
    assert(A' ≠ O ∧ (Par_strict O E A' B ∨ B = O)).
      apply(sum_par_strict A B B A' B);auto.
        repeat split; auto.
      unfold Pj.
      auto.
    spliter.
    induction H15.
      apply False_ind.
      apply H15.
      ∃ B.
      split; Col.
    subst B.
    induction H2.
      induction H2.
        apply False_ind.
        apply H2.
        ∃ O.
        split; Col.
      spliter.
      apply False_ind.
      apply H.
      ColR.
    subst A'.
    tauto.
Qed.

Lemma sum_uniquenessB : ∀ A X Y C, Sum O E E' A X C → Sum O E E' A Y C → X = Y.
Proof.
    intros.
    induction (eq_dec_points A O).
      subst A.
      assert(X = C).
        apply(sum_O_B_eq X C H).
      assert(Y = C).
        apply(sum_O_B_eq Y C H0).
      subst X.
      subst Y.
      auto.
    assert(HSx:= H).
    assert(HSy:= H0).
    unfold Sum in H.
    unfold Sum in H0.
    spliter.
    assert(Hx:=H).
    assert(Hy:=H0).
    unfold Ar2 in H.
    unfold Ar2 in H0.
    spliter.
    ex_and H2 A''.
    ex_and H10 C''.
    ex_and H3 A'.
    ex_and H14 C'.
    clean_duplicated_hyps.
    assert(A' ≠ O ∧ (Par_strict O E A' C' ∨ X = O)).
      apply(sum_par_strict A X C A' C'); auto.
    assert(A'' ≠ O ∧ (Par_strict O E A'' C'' ∨ Y = O)).
      apply(sum_par_strict A Y C A'' C''); auto.
    spliter.
    unfold Pj in ×.
    induction(eq_dec_points X O).
      subst X.
      assert(HH:=sum_A_O A H7).
      assert(C = A).
        apply (sum_uniqueness A O); auto.
      subst C.
      assert(Y=O).
        apply (sum_A_B_A A ); auto.
      subst Y.
      auto.
    induction H2.
      induction H3.
        assert(Par A A' A A'').
          apply (par_trans _ _ E E'); Par.
        induction H19.
          apply False_ind.
          apply H19.
          ∃ A.
          split; Col.
        spliter.
        assert(A' = A'').
          apply (l6_21 O E' A A'); Col.
          intro.
          apply grid_ok.
          apply(col_transitivity_1 _ A); Col.
        subst A''.
        induction H4.
          induction H6.
            assert(Par A' C' A' C'').
              apply(par_trans _ _ O E); left; Par.
            induction H23.
              apply False_ind.
              apply H23.
              ∃ A'.
              split; Col.
            spliter.
            induction H13.
              induction H17.
                assert(Par C C' C C'').
                  apply(par_trans _ _ E' E); Par.
                induction H27.
                  apply False_ind.
                  apply H27.
                  ∃ C.
                  split; Col.
                spliter.
                assert(C' = C'').
                  apply (l6_21 A' C' C C'); Col.
                  intro.
                  apply H6.
                  ∃ C.
                  split; Col.
                subst C''.
                clean_trivial_hyps.
                induction H12.
                  induction H16.
                    assert(Par Y C' X C').
                      apply (par_trans _ _ O E'); Par.
                    induction H21.
                      apply False_ind.
                      apply H21.
                      ∃ C'.
                      split; Col.
                    spliter.
                    apply(l6_21 O E C' X); Col.
                    intro.
                    apply H4.
                    ∃ C'.
                    split; Col.
                  subst X.
                  clean_duplicated_hyps.
                  apply False_ind.
                  apply H6.
                  ∃ C'.
                  split; Col.
                subst Y.
                apply False_ind.
                apply H6.
                ∃ C'.
                split; Col.
              subst C'.
              clean_duplicated_hyps.
              clean_trivial_hyps.
              apply False_ind.
              apply H6.
              ∃ C.
              split; Col.
            subst C''.
            apply False_ind.
            apply H4.
            ∃ C.
            split; Col.
          subst X.
          tauto.
        subst Y.
        assert(A = C).
          apply(sum_A_O_eq A C HSy).
        subst C.
        clean_duplicated_hyps.
        clean_trivial_hyps.
        apply(sum_A_B_A A); auto.
      subst A'.
      clean_duplicated_hyps.
      induction H15.
        induction H6.
          apply False_ind.
          apply H3.
          ∃ A.
          split; Col.
        subst X.
        tauto.
      subst C'.
      induction H6.
        apply False_ind.
        apply H.
        ∃ A.
        split; Col.
      contradiction.
    subst A''.
    induction H4.
      apply False_ind.
      apply H2.
      ∃ A.
      split; Col.
    subst Y.
    assert(A = C).
      apply (sum_A_O_eq A C HSy).
    subst C.
    apply (sum_A_B_A A _ HSx).
Qed.

Lemma sum_uniquenessA : ∀ B X Y C, Sum O E E' X B C → Sum O E E' Y B C → X = Y.
Proof.
    intros.
    induction (eq_dec_points B O).
      subst B.
      assert(X = C).
        apply(sum_A_O_eq X C H).
      subst X.
      assert(Y = C).
        apply(sum_A_O_eq Y C H0).
      subst Y.
      auto.
    assert(HSx:= H).
    assert(HSy:= H0).
    unfold Sum in H.
    unfold Sum in H0.
    spliter.
    assert(Hx:=H).
    assert(Hy:=H0).
    unfold Ar2 in H.
    unfold Ar2 in H0.
    spliter.
    ex_and H2 A''.
    ex_and H10 C''.
    ex_and H3 A'.
    ex_and H14 C'.
    clean_duplicated_hyps.
    unfold Pj in ×.
    induction(eq_dec_points X O).
      subst X.
      assert(HH:=sum_O_B B H8).
      assert(B = C).
        apply (sum_uniqueness O B); auto.
      subst C.
      apply sym_equal.
      apply (sum_A_B_B Y B); auto.
    induction(eq_dec_points Y O).
      subst Y.
      assert(HH:=sum_O_B B H8).
      assert(B = C).
        apply (sum_uniqueness O B); auto.
      subst C.
      apply (sum_A_B_B X B); auto.
    assert(A' ≠ O ∧ (Par_strict O E A' C' ∨ B = O)).
      apply(sum_par_strict X B C A' C'); auto.
    assert(A'' ≠ O ∧ (Par_strict O E A'' C'' ∨ B = O)).
      apply(sum_par_strict Y B C A'' C''); auto.
    spliter.
    induction H12.
      induction H16.
        assert(Par B C' B C'').
          apply (par_trans _ _ O E'); Par.
        induction H20.
          apply False_ind.
          apply H20.
          ∃ B.
          split; Col.
        spliter.
        clean_trivial_hyps.
        induction H13.
          induction H17.
            assert(Par C C' C C'').
              apply (par_trans _ _ E E'); Par.
            induction H22.
              apply False_ind.
              apply H22.
              ∃ C.
              split; Col.
            spliter.
            assert(C' = C'').
              apply(l6_21 C C' B C'); Col.
              intro.
              induction H19.
                apply H19.
                ∃ C'.
                split.
                  assert(Col O B C).
                    apply (col_transitivity_1 _ E); Col.
                    intro.
                    apply grid_ok.
                    subst E.
                    Col.
                  assert(Col E B C).
                    apply (col_transitivity_1 _ O); Col.
                    intro.
                    apply grid_ok.
                    subst E.
                    Col.
                  apply(col3 B C); Col.
                  intro.
                  subst C.
                  clean_trivial_hyps.
                  apply(sum_A_B_B) in HSx.
                  contradiction.
                Col.
              contradiction.
            subst C''.
            clean_trivial_hyps.
            induction H19.
              induction H18.
                assert(Par A' C' A'' C').
                  apply (par_trans _ _ O E);left; Par.
                induction H23.
                  apply False_ind.
                  apply H23.
                  ∃ C'.
                  split; Col.
                spliter.
                assert(A'= A'').
                  apply (l6_21 O E' C' A'); Col.
                  intro.
                  induction H16.
                    apply H16.
                    ∃ C'.
                    split; Col.
                  spliter.
                  apply H1.
                  apply (l6_21 O E C' O); Col.
                    intro.
                    apply grid_ok.
                    ColR.
                  intro.
                  subst C'.
                  clean_trivial_hyps.
                  apply H18.
                  ∃ O.
                  split; Col.
                subst A''.
                clean_trivial_hyps.
                clean_duplicated_hyps.
                induction H2.
                  induction H3.
                    assert(Par Y A' X A').
                      apply(par_trans _ _ E E'); Par.
                    induction H6.
                      apply False_ind.
                      apply H6.
                      ∃ A'.
                      split; Col.
                    spliter.
                    apply (l6_21 O E A' X); Col.
                    intro.
                    apply H19.
                    ∃ A'.
                    split; Col.
                  subst X.
                  apply False_ind.
                  apply H19.
                  ∃ A'.
                  split; Col.
                subst Y.
                apply False_ind.
                apply H19.
                ∃ A'.
                split; Col.
              contradiction.
            contradiction.
          subst C'.
          apply False_ind.
          induction H16.
            apply H16.
            ∃ O.
            split.
              Col.
            apply(col3 O E); Col.
            intro.
            subst E.
            apply grid_ok; Col.
          spliter.
          assert(Col E B C).
            apply (col3 O E); Col.
            intro.
            subst E.
            apply grid_ok; Col.
          apply grid_ok.
          apply(col3 B C); Col.
        subst C''.
        apply False_ind.
        induction H12.
          apply H12.
          ∃ O.
          split.
            Col.
          apply(col3 O E); Col.
          intro.
          subst E.
          apply grid_ok; Col.
        spliter.
        assert(Col E B C).
          apply (col3 O E); Col.
          intro.
          subst E.
          apply grid_ok; Col.
        apply grid_ok.
        apply(col3 B C); Col.
      apply False_ind.
      subst C'.
      induction H19.
        apply H16.
        ∃ B.
        split; Col.
      contradiction.
    subst C''.
    apply False_ind.
    induction H18.
      apply H12.
      ∃ B.
      split; Col.
    contradiction.
Qed.

Lemma sum_B_null : ∀ A B, Sum O E E' A B A → B = O.
Proof.
    intros.
    assert(HS:=H).
    unfold Sum in H.
    spliter.
    unfold Ar2 in H.
    spliter.
    assert(HP:= sum_A_O A H1).
    apply(sum_uniquenessB A B O A); auto.
Qed.

Lemma sum_A_null : ∀ A B, Sum O E E' A B B → A = O.
Proof.
    intros.
    assert(HS:=H).
    unfold Sum in H.
    spliter.
    unfold Ar2 in H.
    spliter.
    assert(HP:= sum_O_B B H2).
    apply(sum_uniquenessA B A O B); auto.
Qed.

Lemma sum_plg : ∀ A B C, Sum O E E' A B C → (A ≠ O ) ∨ ( B ≠ O) → ∃ A', ∃ C', Plg O B C' A' ∧ Plg C' A' A C.
Proof.
    intros.
    assert(HS:=H).
    unfold Sum in H.
    spliter.
    ex_and H1 A'.
    ex_and H2 C'.
    ∃ A'.
    ∃ C'.
    unfold Pj in ×.
    unfold Ar2 in H.
    assert(HH:= grid_not_par).
    spliter.
    induction(eq_dec_points O B).
      subst B.
      assert(HH:=sum_A_O A H12).
      assert(HP:=sum_uniqueness A O C A HS HH).
      subst C.
      induction H4.
        induction H4.
          apply False_ind.
          apply H4.
          ∃ O.
          split; Col.
        spliter.
        induction H3.
          induction H3.
            apply False_ind.
            apply H3.
            ∃ O.
            split.
              Col.
            apply (col_transitivity_1 _ E'); Col.
          spliter.
          apply False_ind.
          apply grid_ok.
          assert(Col C' O E).
            ColR.
          ColR.
        subst C'.
        split; apply parallelogram_to_plg; apply plg_trivial1.
          auto.
        intro.
        subst A'.
        apply H.
        ColR.
      subst C'.
      apply False_ind.
      induction H5.
        apply H6.
        apply par_symmetry.
        apply (par_col_par _ _ _ A); Col; Par.
      subst A.
      induction H0; tauto.
    induction(eq_dec_points A O).
      subst A.
      assert(HH:=sum_O_B B H13 ).
      assert(HP:=sum_uniqueness O B C B HS HH).
      subst C.
      clean_trivial_hyps.
      induction H1.
        induction H1.
          apply False_ind.
          apply H1.
          ∃ E'.
          split; Col.
        spliter.
        apply False_ind.
        apply H.
        apply (col_transitivity_1 _ A'); Col.
      subst A'.
      clean_trivial_hyps.
      induction H5.
        induction H4.
          apply False_ind.
          apply H8.
          apply (par_trans _ _ B C'); Par.
        subst C'.
        split; apply parallelogram_to_plg; apply plg_trivial; auto.
      subst C'.
      split; apply parallelogram_to_plg; apply plg_trivial; auto.
    assert(A' ≠ O).
      intro.
      subst A'.
      induction H1.
        apply H6.
        apply par_symmetry.
        apply (par_col_par _ _ _ A); Col;Par.
      contradiction.
    assert(A' ≠ O ∧ (Par_strict O E A' C' ∨ B = O)).
      apply(sum_par_strict A B C A' C');auto.
      repeat split; auto.
    spliter.
    induction H19.
      assert(Par O B C' A').
        apply par_symmetry.
        apply (par_col_par _ _ _ E); finish.
      assert(Par_strict O B C' A').
        induction H20.
          auto.
        spliter.
        apply False_ind.
        apply H19.
        ∃ O.
        split; Col.
      induction H4.
        assert(Par O A' B C').
          apply par_symmetry.
          apply (par_col_par _ _ _ E'); Par; Col.
        assert(HX:= pars_par_plg O B C' A' H21 H22).
        assert(Par C' A' A C).
          apply(par_col_par _ _ _ O).
            intro.
            subst C.
            apply H15.
            apply sym_equal.
            apply(sum_A_B_A A); auto.
            apply par_right_comm.
            apply(par_col_par _ _ _ B).
              auto.
              Par.
            ColR.
          ColR.
        assert(Par_strict C' A' A C).
          induction H23.
            auto.
          spliter.
          apply False_ind.
          apply H19.
          ∃ C'.
          split.
            ColR.
          Col.
        induction H1.
          induction H5.
            assert(Par C' C A' A).
              apply (par_trans _ _ E E'); Par.
            assert(HY:= pars_par_plg C' A' A C H24 H25).
            split; auto.
          subst C'.
          assert_diffs;contradiction.
        split; Col.
        subst A'.
        assert_diffs.
        contradiction.
      subst C'.
      assert_diffs.
      contradiction.
    subst B.
    tauto.
Qed.

Lemma sum_cong : ∀ A B C, Sum O E E' A B C → (A ≠ O ∨ B ≠ O) → Parallelogram_flat O A C B.
Proof.
    intros.
    induction(eq_dec_points A O).
      subst A.
      assert(HP:= (sum_O_B_eq B C H)).
      subst C.
      induction H0.
        tauto.
      assert(Parallelogram O O B B).
        apply plg_trivial1; auto.
      induction H1.
        apply False_ind.
        unfold Parallelogram_strict in H1.
        spliter.
        apply par_distincts in H2.
        tauto.
      assumption.
    assert(∃ A' C' : Tpoint, Plg O B C' A' ∧ Plg C' A' A C).
      apply(sum_plg A B C); auto.
    ex_and H2 A'.
    ex_and H3 C'.
    apply plg_to_parallelogram in H2.
    apply plg_to_parallelogram in H3.
    apply plgf_permut.
    assert(HH:=plg_pseudo_trans O B C' A' A C H2 H3).
    induction HH.
      induction H4.
        apply False_ind.
        apply H4.
        unfold Sum in H.
        spliter.
        unfold Ar2 in H.
        spliter.
        assert_diffs.
        ColR.
      apply plgf_comm2.
      auto.
    spliter.
    subst A.
    apply False_ind.
    subst C.
    tauto.
Qed.

Lemma sum_cong2 : ∀ A B C,
  Sum O E E' A B C →
  (A ≠ O ∨ B ≠ O) →
  (Cong O A B C ∧ Cong O B A C).
Proof.
intros.
apply sum_cong in H.
unfold Parallelogram_flat in ×.
spliter;split;Cong.
assumption.
Qed.

Lemma sum_comm : ∀ A B C, Sum O E E' A B C → Sum O E E' B A C.
Proof.
    intros.
    induction (eq_dec_points B O).
      subst B.
      assert(Col O E A).
        unfold Sum in H.
        spliter.
        unfold Ar2 in H.
        tauto.
      assert(C = A).
        apply (sum_uniqueness A O).
          auto.
        apply sum_A_O.
        auto.
      subst C.
      apply sum_O_B.
      auto.
    induction(eq_dec_points A O).
      subst A.
      assert(Col O E B).
        unfold Sum in H.
        spliter.
        unfold Ar2 in H.
        tauto.
      assert(B = C).
        apply (sum_uniqueness O B).
          apply sum_O_B.
          Col.
        auto.
      subst C.
      apply sum_A_O.
      Col.
    assert(A ≠ O ∨ B ≠ O).
      left.
      auto.
    assert(HH:=grid_not_par).
    spliter.
    assert(HH := sum_plg A B C H H2).
    ex_and HH A'.
    ex_and H9 C'.
    assert(∃ ! P' : Tpoint, Proj B P' O E' E E').
      apply(project_existence B O E' E E'); auto.
      intro.
      apply H5.
      Par.
    unfold unique in H11.
    ex_and H11 B'.
    clear H12.
    assert(HH:= parallel_existence1 O E B' H6).
    ex_and HH P'.
    assert(∃! P : Tpoint, Proj A P B' P' O E').
      apply(project_existence A B' P' O E'); auto.
      apply par_distincts in H12.
      spliter.
      auto.
      intro.
      apply H4.
      apply(par_trans _ _ B' P'); Par.
    unfold unique in H13.
    ex_and H13 D'.
    clear H14.
    assert( Ar2 O E E' A B C).
      unfold Sum in H.
      tauto.
    assert(HH:= sum_to_sump O E E' A B C H).
    unfold Sump in H13.
    apply sump_to_sum.
    unfold Sump.
    unfold Ar2 in H14.
    spliter.
    repeat split; Col.
    ∃ B'.
    ∃ D'.
    ∃ P'.
    split; auto.
    split; auto.
    split; auto.
    assert(Par_strict O E B' P').
      induction H12.
        auto.
      spliter.
      apply False_ind.
      assert(HA:=H11).
      unfold Proj in H11.
      spliter.
      assert(Col B' O E).
        apply (col_transitivity_1 _ P'); Col.
      assert(B' ≠ O).
        intro.
        subst B'.
        apply project_id in HA.
          contradiction.
        induction H24.
          induction H24.
            apply False_ind.
            apply H24.
            ∃ E.
            split; Col.
          spliter.
          contradiction.
        contradiction.
      apply grid_ok.
      apply (col_transitivity_1 _ B'); Col.
    assert(Par O A B' D').
      apply (par_col_par _ _ _ P').
        intro.
        subst D'.
        unfold Proj in ×.
        spliter.
        induction H22.
          induction H22.
            apply H22.
            ∃ B'.
            split; Col.
          spliter.
          apply grid_ok.
          apply (col_transitivity_1 _ A); Col.
        subst B'.
        apply H18.
        ∃ A.
        split; Col.
        apply par_symmetry.
        apply (par_col_par _ _ _ E); Col; Par.
      unfold Proj in H13.
      spliter.
      Col.
    assert(Par_strict O A B' D').
      induction H19.
        auto.
      spliter.
      apply False_ind.
      apply H18.
      unfold Proj in H13.
      spliter.
      ∃ O.
      split.
        Col.
      apply col_permutation_2.
      apply (col_transitivity_1 _ D'); Col.
    assert(Par O B' A D').
      unfold Proj in H13.
      spliter.
      induction H24.
        apply par_symmetry.
        apply(par_col_par _ _ _ E'); Par.
          intro.
          subst B'.
          apply H20.
          ∃ O.
          split;Col.
        unfold Proj in H11.
        spliter.
        auto.
      subst D'.
      apply False_ind.
      apply H20.
      ∃ A.
      split; Col.
    assert(Plg O A D' B').
      apply(pars_par_plg O A D' B' ); Par.
    assert(HT:=sum_cong A B C H H2).
    assert(Parallelogram D' B' B C ∨ D' = B' ∧ O = A ∧ C = B ∧ D' = C).
      apply(plg_pseudo_trans D' B' O A C B).
        apply plg_to_parallelogram in H22.
        apply plg_permut in H22.
        apply plg_permut in H22.
        auto.
      right.
      auto.
    induction H23.
      repeat split; auto.
      apply plg_permut in H23.
      apply plg_par in H23.
        unfold Proj in ×.
        spliter.
        induction H32.
          left.
          apply (par_trans _ _ B B'); Par.
        subst B'.
        apply par_distincts in H23.
        tauto.
        intro.
        subst B'.
        apply H20.
        ∃ B.
        split.
          ColR.
        Col.
      intro.
      subst C.
      assert(HN:= sum_A_null A B H).
      contradiction.
    spliter.
    subst A.
    tauto.
Qed.

Lemma cong_sum : ∀ A B C,
  O ≠ C ∨ B ≠ A → Ar2 O E E' A B C →
  Cong O A B C → Cong O B A C →
  Sum O E E' A B C.
Proof.
    intros A B C.
    intro Hor.
    intros.
    induction (eq_dec_points A O).
      subst A.
      unfold Ar2 in H.
      spliter.
      apply cong_symmetry in H0.
      apply cong_identity in H0.
      subst C.
      apply sum_O_B; Col.
    induction (eq_dec_points B O).
      subst B.
      unfold Ar2 in H.
      spliter.
      apply cong_symmetry in H1.
      apply cong_identity in H1.
      subst C.
      apply sum_A_O; Col.
    unfold Sum.
    split; auto.
    unfold Ar2 in H.
    assert(HH:=grid_not_par).
    spliter.
    assert(∃ ! P' : Tpoint, Proj A P' O E' E E').
      apply(project_existence A O E' E E'); auto.
      intro.
      apply H6.
      Par.
    ex_and H13 A'.
    unfold unique in H14.
    spliter.
    clear H14.
    unfold Proj in H13.
    spliter.
    clean_duplicated_hyps.
    assert(HH:=parallel_existence1 O E A' H7).
    ex_and HH P'.
    assert(∃ ! C' : Tpoint, Proj B C' A' P' O E').
      apply(project_existence B A' P' O E'); auto.
      apply par_distincts in H.
      spliter.
      auto.
      intro.
      apply H5.
      apply(par_trans _ _ A' P'); Par.
    ex_and H13 C'.
    unfold unique in H14.
    spliter.
    clear H14.
    unfold Proj in H13.
    spliter.
    ∃ A'.
    ∃ C'.
    assert(A' ≠ O).
      intro.
      subst A'.
      induction H17.
        induction H17.
          apply H17.
          ∃ E.
          split; Col.
        spliter.
        contradiction.
      contradiction.
    assert(Par_strict O E A' P').
      unfold Par_strict.
      repeat split; auto; try apply all_coplanar.
      intro.
      ex_and H21 X.
      induction H.
        apply H.
        ∃ X.
        split; Col.
      spliter.
      apply grid_ok.
      ColR.
    assert(A ≠ A').
      intro.
      subst A'.
      apply H21.
      ∃ A.
      split; Col.
    repeat split; Col.
      induction H17.
        left; Par.
      right; auto.
      left.
      apply (par_col_par _ _ _ P').
        intro.
        subst C'.
        induction H19.
          induction H19.
            apply H19.
            ∃ A'.
            split; Col.
          spliter.
          apply grid_ok.
          ColR.
        subst A'.
        apply H21.
        ∃ B.
        split; Col.
        Par.
      Col.
      induction H19.
        left.
        Par.
      right.
      auto.
    assert(A' ≠ C').
      intro.
      subst C'.
      induction H19.
        induction H19.
          apply H19.
          ∃ A'.
          split; Col.
        spliter.
        apply grid_ok.
        ColR.
      subst A'.
      apply H21.
      ∃ B.
      split; Col.
    assert(Plg O B C' A').
      apply(pars_par_plg O B C' A').
        apply par_strict_right_comm.
        apply(par_strict_col_par_strict _ _ _ P').
          auto.
          apply par_strict_symmetry.
          apply(par_strict_col_par_strict _ _ _ E).
            auto.
            Par.
          Col.
        Col.
      induction H19.
        apply par_symmetry.
        apply(par_col_par _ _ _ E').
          auto.
          Par.
        Col.
      subst C'.
      apply False_ind.
      apply H21.
      ∃ B.
      split; Col.
    assert(Plg O B C A).
      apply(parallelogram_to_plg).
      right.
      unfold Parallelogram_flat.
      repeat split; try ColR.
        Cong.
        Cong.
      auto.
    apply plg_to_parallelogram in H24.
    apply plg_to_parallelogram in H25.
    assert(Parallelogram A C C' A').
      assert(Parallelogram C A A' C' ∨ C = A ∧ O = B ∧ C' = A' ∧ C = C').
        apply(plg_pseudo_trans C A O B C' A').
          apply plg_permut.
          apply plg_permut.
          assumption.
        assumption.
      induction H26.
        apply plg_comm2.
        assumption.
      spliter.
      subst C'.
      subst A'.
      tauto.
    apply plg_par in H26.
      spliter.
      induction H17.
        left.
        apply(par_trans _ _ A A'); Par.
      contradiction.
      intro.
      subst C.
      apply cong_identity in H1.
      subst B.
      tauto.
    intro.
    subst C'.
    apply plg_permut in H26.
    induction H19.
      induction H19.
        apply H19.
        ∃ O.
        split; Col.
        ColR.
      spliter.
      apply grid_ok.
      ColR.
    subst C.
    apply H21.
    ∃ B.
    split; Col.
Qed.

Lemma sum_iff_cong : ∀ A B C,
  Ar2 O E E' A B C → (O ≠ C ∨ B ≠ A) →
 ((Cong O A B C ∧ Cong O B A C) ↔ Sum O E E' A B C).
Proof.
intros.
split.
intros.
apply cong_sum;intuition idtac.
intros.
apply sum_cong2.
assumption.
destruct H.
elim (eq_dec_points A O); intro.
subst.
right.
intro.
subst.
assert (T:= sum_O_O).
destruct H0.
apply H0.
eauto using sum_uniqueness.
intuition.
intuition.
Qed.

Lemma opp_comm : ∀ X Y, Opp O E E' X Y → Opp O E E' Y X.
Proof.
    intros.
    unfold Opp in ×.
    apply sum_comm.
    auto.
Qed.

Lemma opp_uniqueness :
 ∀ A MA1 MA2,
 Opp O E E' A MA1 →
 Opp O E E' A MA2 →
 MA1 = MA2.
Proof.
    intros.
    unfold Opp in ×.
    apply sum_comm in H.
    apply sum_comm in H0.
    induction(eq_dec_points A O).
      subst A.
      assert(HH:=sum_uniquenessB O MA1 MA2 O H H0).
      assumption.
    apply sum_plg in H.
      apply sum_plg in H0.
        ex_and H A'.
        ex_and H2 C'.
        ex_and H0 A''.
        ex_and H3 C''.
        apply plg_to_parallelogram in H.
        apply plg_to_parallelogram in H0.
        apply plg_to_parallelogram in H2.
        apply plg_to_parallelogram in H3.
        assert(Parallelogram C' A' A'' C'' ∨ C' = A' ∧ A = O ∧ C'' = A'' ∧ C' = C'').
          apply(plg_pseudo_trans C' A' A O C'' A''); auto.
          apply plg_permut.
          apply plg_permut.
          auto.
        induction H4.
          assert(Parallelogram O MA1 C'' A'' ∨ O = MA1 ∧ C' = A' ∧ A'' = C'' ∧ O = A'').
            apply(plg_pseudo_trans O MA1 C' A' A'' C''); auto.
          induction H5.
            assert(Parallelogram O MA1 MA2 O ∨ O = MA1 ∧ C'' = A'' ∧ O = MA2 ∧ O = O).
              apply(plg_pseudo_trans O MA1 C'' A'' O MA2); auto.
              apply plg_permut.
              apply plg_permut.
              assumption.
            induction H6.
              unfold Parallelogram in H6.
              induction H6.
                unfold Parallelogram_strict in H6.
                spliter.
                unfold TS in H6.
                spliter.
                apply False_ind.
                apply H9.
                Col.
              unfold Parallelogram_flat in H6.
              spliter.
              apply cong_symmetry in H9.
              apply cong_identity in H9.
              auto.
            spliter.
            subst MA1.
            subst MA2.
            auto.
          spliter.
          subst MA1.
          subst C''.
          subst A''.
          subst C'.
          unfold Parallelogram in H0.
          induction H0.
            unfold Parallelogram_strict in H0.
            spliter.
            apply par_distincts in H5.
            tauto.
          unfold Parallelogram_flat in H0.
          spliter.
          apply cong_identity in H6.
          auto.
        spliter.
        contradiction.
      left; auto.
    left; auto.
Qed.

End Grid.

Lemma pj_uniqueness : ∀ O E E' A A' A'', ¬Col O E E' → Col O E A → Col O E' A' → Col O E' A'' → Pj E E' A A' → Pj E E' A A'' → A' = A''.
Proof.
    intros.
    unfold Pj in ×.
    induction(eq_dec_points A O).
      subst A.
      assert(HH:= grid_not_par O E E' H).
      spliter.
      induction H3.
        apply False_ind.
        apply H7.
        apply par_symmetry.
        apply (par_col_par _ _ _ A'); Col.
      subst A'.
      induction H4.
        apply False_ind.
        apply H7.
        apply par_symmetry.
        apply (par_col_par _ _ _ A''); Col.
      auto.
    induction H3; induction H4.
      assert(Par A A' A A'').
        apply (par_trans _ _ E E'); Par.
      induction H6.
        apply False_ind.
        apply H6.
        ∃ A.
        split; Col.
      spliter.
      apply(l6_21 O E' A A'); Col.
      intro.
      apply H.
      ColR.
      auto.
      subst A''.
      apply False_ind.
      apply H.
      ColR.
      auto.
      subst A'.
      apply False_ind.
      apply H.
      ColR.
    congruence.
Qed.

Lemma pj_right_comm : ∀ A B C D, Pj A B C D → Pj A B D C.
Proof.
    intros.
    unfold Pj in ×.
    induction H.
      left.
      Par.
    right.
    auto.
Qed.

Lemma pj_left_comm : ∀ A B C D, Pj A B C D → Pj B A C D.
Proof.
    intros.
    unfold Pj in ×.
    induction H.
      left.
      Par.
    right.
    auto.
Qed.

Lemma pj_comm : ∀ A B C D, Pj A B C D → Pj B A D C.
Proof.
    intros.
    apply pj_left_comm.
    apply pj_right_comm.
    auto.
Qed.