Library GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec

Require Export GeoCoq.Tarski_dev.Ch12_parallel_inter_dec.
Require Export GeoCoq.Tarski_dev.Annexes.Tagged_predicates.

Ltac image_6 A B P' H P:=
 let T:= fresh in assert (T:= l10_6_existence A B P' H);
 ex_and T P.

Ltac image A B P P':=
 let T:= fresh in assert (T:= l10_2_existence A B P);
 ex_and T P'.

Ltac perp A B C X :=
 match goal with
   | H:(¬Col A B C) |- _
    let T:= fresh in assert (T:= l8_18_existence A B C H);
    ex_and T X
 end.

Ltac parallel A B C D P :=
 match goal with
   | H:(A B) |- _
    let T := fresh in assert(T:= parallel_existence A B P H);
    ex_and T C
 end.

Ltac par_strict :=
repeat
 match goal with
      | H: Par_strict ?A ?B ?C ?D |- _
       let T := fresh in not_exist_hyp (Par_strict B A D C); assert (T := par_strict_comm A B C D H)
      | H: Par_strict ?A ?B ?C ?D |- _
       let T := fresh in not_exist_hyp (Par_strict C D A B); assert (T := par_strict_symmetry A B C D H)
      | H: Par_strict ?A ?B ?C ?D |- _
       let T := fresh in not_exist_hyp (Par_strict B A C D); assert (T := par_strict_left_comm A B C D H)
      | H: Par_strict ?A ?B ?C ?D |- _
       let T := fresh in not_exist_hyp (Par_strict A B D C); assert (T := par_strict_right_comm A B C D H)
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _clear H
   | H:(Col ?X1 ?X1 ?X2) |- _clear H
   | H:(Col ?X2 ?X1 ?X1) |- _clear H
   | H:(Col ?X1 ?X2 ?X1) |- _clear H
   | H:(Par ?X1 ?X2 ?X1 ?X2) |- _clear H
   | H:(Par ?X1 ?X2 ?X2 ?X1) |- _clear H
   | H:(Per ?X1 ?X2 ?X2) |- _clear H
   | H:(Per ?X1 ?X1 ?X2) |- _clear H
   | H:(Midpoint ?X1 ?X1 ?X1) |- _clear H
end.

Ltac show_distinct2 := unfold not;intro;treat_equalities; try (solve [intuition]).

Ltac symmetric A B A' :=
 let T := fresh in assert(T:= symmetric_point_construction A B);
 ex_and T A'.

Tactic Notation "Name" ident(X) "the" "symmetric" "of" ident(A) "wrt" ident(C) :=
 symmetric A C X.

Ltac sfinish := repeat match goal with
 | |- Bet ?A ?B ?CBetween; eBetween
 | |- Col ?A ?B ?CCol;ColR
 | |- ¬ Col ?A ?B ?CCol
 | |- ¬ Col ?A ?B ?Cintro;search_contradiction
 | |- Par ?A ?B ?C ?DPar
 | |- Par_strict ?A ?B ?C ?DPar
 | |- Perp ?A ?B ?C ?DPerp
 | |- Perp_at ?A ?B ?C ?D ?EPerp
 | |- Per ?A ?B ?CPerp
 | |- Cong ?A ?B ?C ?DCong;eCong
 | |- Midpoint ?A ?B ?CMidpoint
 | |- ?A?Bapply swap_diff;assumption
 | |- ?A?Bintro;treat_equalities; solve [search_contradiction]
 | |- ?G1 ?G2split
 | |- _try assumption
end.

Ltac clean_reap_hyps :=
  repeat
  match goal with
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?A ?B ?D ?C |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?A ?B ?C ?D |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?C ?D ?A ?B |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?C ?D ?B ?A |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?D ?C ?B ?A |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?D ?C ?A ?B |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?B ?A ?C ?D |- _clear H2
   | H:(Parallelogram ?A ?B ?C ?D), H2 : Parallelogram ?B ?A ?D ?C |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?A ?B ?D ?C |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?A ?B ?C ?D |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?C ?D ?A ?B |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?C ?D ?B ?A |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?D ?C ?B ?A |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?D ?C ?A ?B |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?B ?A ?C ?D |- _clear H2
   | H:(Par ?A ?B ?C ?D), H2 : Par ?B ?A ?D ?C |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?A ?B ?D ?C |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?A ?B ?C ?D |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?C ?D ?A ?B |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?C ?D ?B ?A |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?D ?C ?B ?A |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?D ?C ?A ?B |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?B ?A ?C ?D |- _clear H2
   | H:(Par_strict ?A ?B ?C ?D), H2 : Par_strict ?B ?A ?D ?C |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?A ?B ?D ?C |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?A ?B ?C ?D |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?C ?D ?A ?B |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?C ?D ?B ?A |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?D ?C ?B ?A |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?D ?C ?A ?B |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?B ?A ?C ?D |- _clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?B ?A ?D ?C |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?A ?B ?D ?C |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?A ?B ?C ?D |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?C ?D ?A ?B |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?C ?D ?B ?A |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?D ?C ?B ?A |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?D ?C ?A ?B |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?B ?A ?C ?D |- _clear H2
   | H:(Perp_at ?X ?A ?B ?C ?D), H2 : Perp_at ?X ?B ?A ?D ?C |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?A ?B ?C |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?A ?C ?B |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?B ?A ?C |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?B ?C ?A |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?C ?B ?A |- _clear H2
   | H:(Per ?A ?B ?C), H2 : Per ?C ?A ?B |- _clear H2
   | H:(Midpoint ?A ?B ?C), H2 : Midpoint ?A ?C ?B |- _clear H2
   | H:(Midpoint ?A ?B ?C), H2 : Midpoint ?A ?B ?C |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?B ?A ?C) |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?B ?C ?A) |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?C ?B ?A) |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?C ?A ?B) |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?A ?C ?B) |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : (¬Col ?A ?B ?C) |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _clear H2
   | H:(?A?B), H2 : (?B?A) |- _clear H2
   | H:(?A?B), H2 : (?A?B) |- _clear H2
end.

Ltac tag_hyps :=
  repeat
  match goal with
    | H : ?A ?B |- _apply Diff_Diff_tagged in H
    | H : Cong ?A ?B ?C ?D |- _apply Cong_Cong_tagged in H
    | H : Bet ?A ?B ?C |- _apply Bet_Bet_tagged in H
    | H : Col ?A ?B ?C |- _apply Col_Col_tagged in H
    | H : ¬ Col ?A ?B ?C |- _apply NCol_NCol_tagged in H
    | H : Midpoint ?A ?B ?C |- _apply Mid_Mid_tagged in H
    | H : Per ?A ?B ?C |- _apply Per_Per_tagged in H
    | H : Perp_at ?X ?A ?B ?C ?D |- _apply Perp_in_Perp_in_tagged in H
    | H : Perp ?A ?B ?C ?D |- _apply Perp_Perp_tagged in H
    | H : Par_strict ?A ?B ?C ?D |- _apply Par_strict_Par_strict_tagged in H
    | H : Par ?A ?B ?C ?D |- _apply Par_Par_tagged in H
    | H : Parallelogram ?A ?B ?C ?D |- _apply Plg_Plg_tagged in H
  end.

Ltac permutation_intro_in_goal :=
 match goal with
 | |- Par ?A ?B ?C ?Dapply Par_cases
 | |- Par_strict ?A ?B ?C ?Dapply Par_strict_cases
 | |- Perp ?A ?B ?C ?Dapply Perp_cases
 | |- Perp_at ?X ?A ?B ?C ?Dapply Perp_in_cases
 | |- Per ?A ?B ?Capply Per_cases
 | |- Midpoint ?A ?B ?Capply Mid_cases
 | |- ¬ Col ?A ?B ?Capply NCol_cases
 | |- Col ?A ?B ?Capply Col_cases
 | |- Bet ?A ?B ?Capply Bet_cases
 | |- Cong ?A ?B ?C ?Dapply Cong_cases
 end.

Ltac perm_apply t :=
 permutation_intro_in_goal;
 try_or ltac:(apply t;solve [finish]).

Section Quadrilateral_inter_dec_1.

Context `{TE:Tarski_2D_euclidean}.

Lemma par_cong_mid_ts :
  A B A' B',
  Par_strict A B A' B'
  Cong A B A' B'
  TS A A' B B'
   M, Midpoint M A A' Midpoint M B B'.
Proof.
intros.

assert(HH:= H1).
unfold TS in HH.
assert(¬ Col B A A').
spliter; assumption.
spliter.
ex_and H5 M.
M.

assert(HH:= H).
unfold Par_strict in HH.
spliter.

assert(HH:=(midpoint_existence A A')).
ex_and HH X.

prolong B X B'' B X.
assert(Midpoint X B B'').
unfold Midpoint.
split.
assumption.
Cong.

assert(Par_strict B A B'' A').
apply (midpoint_par_strict B A B'' A' X); auto.

assert(Col B'' B' A' Col A' B' A').
apply(parallel_uniqueness B A B' A' B'' A' A').
apply par_comm.
unfold Par.
left.
assumption.
Col.
unfold Par.
left.
assumption.
Col.
spliter.

assert(Cong A B A' B'').
eapply l7_13.
apply l7_2.
apply H11.
apply l7_2.
assumption.
assert(Cong A' B' A' B'').
eapply cong_transitivity.
apply cong_symmetry.
apply H0.
assumption.

assert(B' = B'' Midpoint A' B' B'').
eapply l7_20.
Col.
Cong.
induction H20.

subst B''.

assert(X = M).
eapply (l6_21 A A' B B'); Col.

intro.
subst B'.
apply H10.
B.
split; Col.
subst X.
split; auto.

assert(TS A A' B B'').
unfold TS.
repeat split; auto.
intro.
apply H4.
apply col_permutation_1.
eapply (col_transitivity_1 _ B'').
intro.
subst B''.
apply l7_2 in H20.
apply is_midpoint_id in H20.
contradiction.
Col.
Col.
X.
split.

unfold Midpoint in H11.
spliter.
apply bet_col in H11.
Col.
assumption.

assert(OS A A' B' B'').
eapply l9_8_1.
apply l9_2.
apply H1.
apply l9_2.
assumption.

assert(TS A A' B' B'').
unfold TS.
repeat split.
intro.
apply H4.
Col.
intro.
apply H4.

apply col_permutation_1.
eapply (col_transitivity_1 _ B'').
intro.
subst B''.
apply l7_2 in H20.
apply is_midpoint_id in H20.
contradiction.
Col.
Col.

A'.
split.
Col.
unfold Midpoint in H20.
spliter.
assumption.
apply l9_9 in H23.
contradiction.
Qed.

Lemma par_cong_mid_os :
   A B A' B',
   Par_strict A B A' B'
   Cong A B A' B'
   OS A A' B B'
    M, Midpoint M A B' Midpoint M B A'.
Proof.
intros.
assert(HH:= H).
unfold Par_strict in HH.
spliter.

assert(HH:=(midpoint_existence A' B)).
ex_and HH X.
X.

prolong A X B'' A X.
assert(Midpoint X A B'').
unfold Midpoint.
split.
assumption.
Cong.

assert(¬Col A B A').
intro.
apply H5.
A'.
split; Col.

assert(Par_strict A B B'' A').
apply (midpoint_par_strict A B B'' A' X).
auto.
assumption.
assumption.
apply l7_2.
assumption.

assert(Col B'' B' A' Col A' B' A').
apply (parallel_uniqueness B A B' A' B'' A' A').

apply par_comm.
unfold Par.
left.
assumption.
Col.
apply par_left_comm.
unfold Par.
left.
assumption.
Col.
spliter.

assert(Cong A B B'' A').
eapply l7_13.
apply l7_2.
apply H9.
assumption.
assert(Cong A' B' A' B'').
eapply cong_transitivity.
apply cong_symmetry.
apply H0.
Cong.
assert(B' = B'' Midpoint A' B' B'').
eapply l7_20.
Col.
Cong.

induction H16.
subst B''.
split.
assumption.
apply l7_2.
assumption.

assert(OS A A' X B'').

eapply (out_one_side_1 _ _ X B'').
intro.
subst A'.
apply H10.
Col.
intro.
apply H10.
apply col_permutation_1.
eapply (col_transitivity_1 _ X).
intro.
subst X.
apply is_midpoint_id in H6.
subst A'.
apply H5.
B.
split; Col.
Col.
unfold Midpoint in H6.
spliter.
apply bet_col in H6.
Col.
Col.
unfold Out.
repeat split.
intro.
subst X.
apply cong_identity in H8.
subst B''.
unfold Par_strict in H11.
spliter.
apply H18.
A.
split; Col.
intro.
subst B''.
unfold Par_strict in H11.
spliter.
apply H19.
A.
split; Col.
unfold Midpoint in H8.
spliter.
left.
assumption.

assert(TS A A' B' B'').
unfold TS.
repeat split.
intro.
apply H5.
A.
split; Col.

unfold OS in H17.
ex_and H17 T.
unfold TS in H18.
spliter.
assumption.
A'.
split.
Col.
unfold Midpoint in H16.
spliter.
assumption.

assert(TS A A' X B').
eapply l9_8_2.
apply l9_2.
apply H18.
apply one_side_symmetry.
assumption.

assert(OS A A' X B).

eapply (out_one_side_1).
intro.
subst A'.
apply H10.
Col.
intro.
apply H10.
apply col_permutation_1.
eapply (col_transitivity_1 _ X).
intro.
subst X.
apply is_midpoint_id in H6.
subst A'.
apply H5.
B.
split; Col.
Col.
unfold Midpoint in H6.
spliter.
apply bet_col in H6.
Col.
apply col_trivial_2;Col.
unfold Out.
repeat split.
intro.
subst X.
unfold TS in H19.
spliter.
apply H19.
Col.
intro.
subst A'.
unfold Par_strict in H11.
spliter.
apply H22.
B.
split; Col.
unfold Midpoint in H6.
spliter.
left.
assumption.

assert(OS A A' X B').
eapply one_side_transitivity.
apply H20.
assumption.
apply l9_9 in H19.
contradiction.
Qed.

Lemma par_strict_cong_mid :
  A B A' B',
  Par_strict A B A' B'
  Cong A B A' B'
   M, Midpoint M A A' Midpoint M B B'
             Midpoint M A B' Midpoint M B A'.
Proof.
intros A B A' B' HParS HCong.
assert (HP:=parallel_uniqueness).
destruct (midpoint_existence A A') as [M1 HM1].
destruct (symmetric_point_construction B M1) as [B'' HB''].
assert (HCol1 : Col B'' A' B').
  {
  assert (Col A' A' B' Col B'' A' B'); try (spliter; Col).
  assert (HPar := par_strict_par A B A' B' HParS);
  apply HP with A B A'; Col; unfold Par_strict in HParS; spliter;
  apply midpoint_par with M1; Col.
  }
assert (HCong1 : Cong A' B' A' B'')
  by (assert (H := l7_13 M1 A' B'' A B HM1 HB''); eCong).
destruct (midpoint_existence A B') as [M2 HM2].
destruct (symmetric_point_construction B M2) as [A'' HA''].
assert (HCol2 : Col A'' A' B').
  {
  assert (Col B' A' B' Col A'' A' B'); try (spliter; Col).
  assert (HPar := par_strict_par A B A' B' HParS);
  apply HP with A B B'; Col; unfold Par_strict in HParS; spliter;
  apply midpoint_par with M2; Col.
  }
assert (HCong2 : Cong A' B' B' A'')
  by (assert (H := l7_13 M2 B' A'' A B HM2 HA''); eCong).
elim (l7_20 A' B' B''); Col; intro HElim1; treat_equalities.

  {
   M1; left; Col.
  }


  {
  elim (l7_20 B' A' A''); Cong; Col; intro HElim2; treat_equalities.

    {
     M2; right; Col.
    }

    {
    exfalso; destruct (outer_pasch B' A A' B'' M1) as [I [HAIB' HA''IM1]];
    unfold Midpoint in*; spliter; Between.
    assert (HM1I : M1 I).
      {
      intro; treat_equalities.
      show_distinct A M1; apply HParS; A; split; Col; assert_cols; ColR.
      }
    assert (HB''M1 : B'' M1).
      {
      intro; treat_equalities; apply HParS; B; assert_cols; Col.
      }
    elim (l5_2 B'' M1 I B); Between; intro HBM1I.

      {
      assert (HFalse : TS A B' B A'').
        {
        split; try (intro; apply HParS; B'; Col).
        show_distinct B' A''; try (apply HParS; A; Col).
        show_distinct A' B'; try (apply HParS; A; Col).
        split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
         M2; assert_cols; Col.
        }
      apply l9_9 in HFalse; apply HFalse; clear HFalse.
       A'; split.

        {
        apply l9_2; apply l9_8_2 with B''.

          {
          show_distinct A' B'; try (apply HParS; A; Col).
          show_distinct B' B''; try (apply HParS; A; Col).
          split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
          split; try (intro; apply HParS; B'; split; Col).
           I; assert_cols; split; Col; eBetween.
          }

          {
          apply l9_19 with B'; Col; try (intro; treat_equalities; apply HParS; A; Col).
          show_distinct A' B'; try (apply HParS; A; Col).
          show_distinct B' B''; try (apply HParS; A; Col).
          split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
          split; Col.
          }
        }

        {
        show_distinct B' A''; try (apply HParS; A; Col).
        show_distinct A' B'; try (apply HParS; A; Col).
        split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
        split; try (intro; apply HParS; A; Col).
         B'; split; Col; Between.
        }
      }

      {
      assert (HFalse : OS A A' B B').
        {
         B''; split.

          {
          split; try (intro; apply HParS; A'; Col).
          show_distinct A' B'; try (apply HParS; A; Col).
          show_distinct A' B''; try (apply HParS; A; Col).
          split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
           M1; assert_cols; Col.
          }

          {
          split; try (intro; apply HParS; A; Col).
          show_distinct A' B'; try (apply HParS; A; Col).
          show_distinct A' B''; try (apply HParS; A; Col).
          split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
           A'; Col.
          }
        }
      apply l9_9_bis in HFalse; apply HFalse; clear HFalse; apply l9_31.

        {
        apply l12_6; Col.
        }

        {
        apply one_side_transitivity with B''.

          {
          apply l9_19 with B'; Col; try (intro; treat_equalities; apply HParS; A; Col).
          split; try (intro; apply HParS; A; Col).
          split; try (intro; treat_equalities; apply HParS; A; Col).
          split; try (intro; treat_equalities; apply HParS; A; Col); Between.
          }

          {
          assert_cols; apply l9_19 with I; Col; try ColR;
          try (intro; treat_equalities; apply HParS; A; Col).
          show_distinct A' B'; try (apply HParS; A; Col).
          show_distinct B' B''; try (apply HParS; A; Col).
          split; try (intro; apply HParS; A; split; Col; assert_cols; ColR).
          split; try (intro; treat_equalities; Col).
          split; try (intro; treat_equalities; apply HParS; assert_cols; B'; Col).
          eBetween.
          }
        }
      }
    }
  }
Qed.

Lemma par_strict_cong_mid1 :
  A B A' B',
  Par_strict A B A' B'
  Cong A B A' B'
  (TS A A' B B' M, Midpoint M A A' Midpoint M B B')
  (OS A A' B B' M, Midpoint M A B' Midpoint M B A').
Proof.
intros.
assert(HH:= H).
unfold Par_strict in HH.
spliter.
assert(TS A A' B B' OS A A' B B').
apply (one_or_two_sides A A' B B').
intro.
apply H4.
A'.
split; Col.
intro.
apply H4.
A.
split; Col.
induction H5.
left.
split.
assumption.
assert(HH:=par_cong_mid_ts A B A' B' H H0 H5).
ex_and HH M.
M.
split; assumption.
right.
split.
assumption.
assert(HH:=par_cong_mid_os A B A' B' H H0 H5).
ex_and HH M.
M.
split; assumption.
Qed.

Lemma par_cong_mid :
  A B A' B',
  Par A B A' B'
  Cong A B A' B'
   M, Midpoint M A A' Midpoint M B B'
             Midpoint M A B' Midpoint M B A'.
Proof.
intros.
induction H.
apply par_strict_cong_mid; try assumption.
apply col_cong_mid.
unfold Par.
right.
assumption.
intro.
unfold Par_strict in H1.
spliter.
apply H4.
A.
split; Col.
assumption.
Qed.

Lemma ts_cong_par_cong_par :
  A B A' B',
 TS A A' B B'
 Cong A B A' B'
 Par A B A' B'
 Cong A B' A' B Par A B' A' B.
Proof.
intros A B A' B' HTS HCong HPar.
assert(HAB : A B) by (intro; treat_equalities; unfold TS in *; spliter; Col).
destruct (par_cong_mid A B A' B') as [M HM]; Col.
elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2].

  {
  assert(HAB' : A B') by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  split; try apply l7_13 with M; try apply l12_17 with M; Midpoint.
  }

  {
  assert(HAA' : A A') by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  assert (HFalse := HTS); apply l9_9 in HFalse; exfalso; apply HFalse; clear HFalse.
  unfold TS in HTS; spliter; apply l12_6; apply par_not_col_strict with B; Col.
  assert (Par A A' B' B); Par; apply l12_17 with M; Midpoint.
  }
Qed.

Lemma plgs_cong :
  A B C D,
 Parallelogram_strict A B C D
 Cong A B C D Cong A D B C.
Proof.
intros A B C D HPara.
destruct HPara as [HTS [HCong HPar]]; split; Col.
destruct (ts_cong_par_cong_par A B C D) as [HCong' HPar']; Cong.
Qed.

Lemma plg_cong :
  A B C D,
  Parallelogram A B C D
 Cong A B C D Cong A D B C.
Proof.
intros.
induction H.
apply plgs_cong.
assumption.
apply plgf_cong.
assumption.
Qed.

Lemma rmb_cong :
  A B C D,
  Rhombus A B C D
  Cong A B B C Cong A B C D Cong A B D A.
Proof.
intros.
unfold Rhombus in H.
spliter.
assert(HH:= plg_to_parallelogram A B C D H).
assert(HH1:= plg_cong A B C D HH).
spliter.
repeat split; eCong.
Qed.

Lemma rmb_per:
  A B C D M,
  Midpoint M A C
  Rhombus A B C D
  Per A M D.
Proof.
intros.
assert(HH:=H0).
unfold Rhombus in HH.
spliter.
assert(HH:=H1).
unfold Plg in HH.
spliter.
ex_and H4 M'.
assert(M = M').
eapply l7_17.
apply H.
assumption.
subst M'.
unfold Per.
B.
split.
apply l7_2.
assumption.
apply rmb_cong in H0.
spliter.
Cong.
Qed.

Lemma per_rmb :
  A B C D M,
  Plg A B C D
  Midpoint M A C
  Per A M B
  Rhombus A B C D.
Proof.
intros.
unfold Per in H1.
ex_and H1 D'.
assert(HH:=H).
unfold Plg in HH.
spliter.
ex_and H4 M'.
assert(M = M').
eapply l7_17.
apply H0.
apply H4.
subst M'.
assert(D = D').
eapply symmetric_point_uniqueness.
apply H5.
assumption.
subst D'.
unfold Rhombus.
split.
assumption.
assert(Cong A D B C).
apply plg_to_parallelogram in H.
assert(HH:=plg_cong A B C D H).
spliter.
assumption.
eapply cong_transitivity.
apply H2.
assumption.
Qed.

Lemma perp_rmb :
  A B C D,
  Plg A B C D
  Perp A C B D
  Rhombus A B C D.
Proof.
intros.
assert(HH:=midpoint_existence A C).
ex_and HH M.
apply (per_rmb A B C D M).
assumption.
assumption.
apply perp_in_per.
unfold Plg in H.
spliter.
ex_and H2 M'.
assert(M = M').
eapply l7_17.
apply H1.
assumption.
subst M'.
assert(Perp A M B M).
eapply perp_col.
intro.
subst M.
apply is_midpoint_id in H1.
subst C.
apply perp_not_eq_1 in H0.
tauto.
apply perp_sym.
eapply perp_col.
intro.
subst M.
apply is_midpoint_id in H3.
subst D.
apply perp_not_eq_2 in H0.
tauto.
apply perp_sym.
apply H0.
unfold Midpoint in H3.
spliter.
apply bet_col in H3.
Col.
unfold Midpoint in H2.
spliter.
apply bet_col in H2.
Col.
apply perp_left_comm in H4.
apply perp_perp_in in H4.
apply perp_in_comm.
assumption.
Qed.

Lemma plg_conga1 : A B C D, A B A C Plg A B C D CongA B A C D C A.
intros.
apply cong3_conga; auto.
assert(HH := plg_to_parallelogram A B C D H1).
apply plg_cong in HH.
spliter.
repeat split; Cong.
Qed.

Lemma os_cong_par_cong_par :
  A B A' B',
  OS A A' B B'
  Cong A B A' B'
  Par A B A' B'
 Cong A A' B B' Par A A' B B'.
Proof.
intros.

induction H1.

assert(A B A A').
unfold OS in H.
ex_and H C.
unfold TS in H.
spliter.
split.
intro.
subst B.
apply H.
Col.
intro.
subst A'.
Col.
spliter.

assert(HH:= (par_strict_cong_mid1 A B A' B' H1 H0 )).
induction HH.
spliter.
apply l9_9 in H4.
contradiction.
spliter.
ex_and H5 M.
assert(HH:= mid_par_cong A B B' A' M H2 H3).
assert(Cong A B B' A' Cong A A' B' B Par A B B' A' Par A A' B' B).
apply HH.
assumption.
assumption.
spliter.
split.
Cong.
Par.
spliter.
unfold OS in H.
ex_and H C.
unfold TS in H5.
spliter.
apply False_ind.
apply H5.
Col.
Qed.

Lemma plgs_permut :
  A B C D,
  Parallelogram_strict A B C D
  Parallelogram_strict B C D A.
Proof.
intros A B C D HPara.
destruct HPara as [HTS [HCong HPar]].
destruct (ts_cong_par_cong_par A B C D) as [HCong' HPar']; Col.
destruct (par_cong_mid A B C D) as [M HM]; Col.
elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2].

  {
  assert (HAM : A M) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  assert (HCM : C M) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  assert (HBD : B D) by (assert (H:=not_two_sides_id B A C); intro; treat_equalities; Col).
  destruct HTS as [HAC [HABC HTS]]; assert_cols.
  repeat try (split; Cong; Par; try (intro; apply HABC; ColR)).
  unfold Midpoint in *; spliter; M; split; Col; Between.
  }

  {
  assert(HAB : A B) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  assert(HAC : A C) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
  assert (HFalse := HTS); apply l9_9 in HFalse; exfalso; apply HFalse; clear HFalse.
  unfold TS in HTS; spliter; apply l12_6; apply par_not_col_strict with B; Col.
  assert (Par A C D B); Par; apply l12_17 with M; Midpoint.
  }
Qed.

Lemma plg_permut :
  A B C D,
  Parallelogram A B C D
  Parallelogram B C D A.
Proof.
intros A B C D HPara.
elim HPara; clear HPara; intro HPara.

  {
  left; apply plgs_permut; Col.
  }

  {right; apply plgf_permut; Col.
  }
Qed.

Lemma plgs_sym :
  A B C D,
  Parallelogram_strict A B C D
  Parallelogram_strict C D A B.
Proof.
intros; do 2 (try (apply plgs_permut; Col)).
Qed.

Lemma plg_sym :
  A B C D,
  Parallelogram A B C D
  Parallelogram C D A B.
Proof.
intros.
unfold Parallelogram in ×.
induction H.
left.
apply plgs_permut.
apply plgs_permut.
assumption.
right.
apply plgf_permut.
apply plgf_permut.
assumption.
Qed.

Lemma plgs_mid :
  A B C D,
  Parallelogram_strict A B C D
   M, Midpoint M A C Midpoint M B D.
Proof.
intros A B C D HPara.
destruct HPara as [HTS [HCong HPar]].
destruct (par_cong_mid A B C D) as [M HM]; Col.
elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2]; try ( M; Col).
assert(HAB : A B) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
assert(HAC : A C) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
assert (HFalse := HTS); apply l9_9 in HFalse; exfalso; apply HFalse; clear HFalse.
unfold TS in HTS; spliter; apply l12_6; apply par_not_col_strict with B; Col.
assert (Par A C D B); Par; apply l12_17 with M; Midpoint.
Qed.

Lemma plg_mid :
  A B C D,
  Parallelogram A B C D
   M, Midpoint M A C Midpoint M B D.
Proof.
intros A B C D HPara.
elim HPara; clear HPara; intro HPara.

  {
  apply plgs_mid; Col.
  }

  {
  apply plgf_mid; Col.
  }

Qed.

Lemma plg_mid_2 :
  A B C D I,
  Parallelogram A B C D
  Midpoint I A C
  Midpoint I B D.
Proof.
intros.
elim (plg_mid A B C D).
intros I' HI'.
spliter.
treat_equalities.
assumption.
assumption.
Qed.

Lemma plgs_not_comm :
   A B C D,
   Parallelogram_strict A B C D
 ¬ Parallelogram_strict A B D C ¬ Parallelogram_strict B A C D.
Proof.
intros.
unfold Parallelogram_strict in ×.
split.
intro.
spliter.
assert(HH:=
ts_cong_par_cong_par A B C D H H4 H3).
spliter.

assert(Par_strict A D C B).
induction H6.
assumption.
spliter.

unfold Par_strict.
repeat split; auto; try apply all_coplanar.
intro.
unfold TS in ×.
spliter.
apply H.
Col.
apply l12_6 in H7.
apply l9_9 in H0.
apply one_side_symmetry in H7.
contradiction.

intro.
spliter.
assert(HH:=ts_cong_par_cong_par A B C D H H4 H3).
spliter.
apply par_symmetry in H6.

assert(Par_strict C B A D).
induction H6.
assumption.
spliter.
unfold Par_strict.
repeat split; auto; try apply all_coplanar.
intro.
unfold TS in ×.
spliter.
apply H13.
Col.
apply l12_6 in H7.
apply l9_9 in H0.
apply invert_one_side in H7.
contradiction.
Qed.

Lemma plg_not_comm :
  A B C D,
 A B
 Parallelogram A B C D
 ¬ Parallelogram A B D C ¬ Parallelogram B A C D.
Proof.
intros.
unfold Parallelogram.
induction H0.
split.
intro.
induction H1.
apply plgs_not_comm in H0.
spliter.
contradiction.
unfold Parallelogram_strict in H0.
spliter.
unfold Parallelogram_flat in H1.
spliter.
apply par_symmetry in H2.
induction H2.
unfold Par_strict in H2.
spliter.
apply H10.
D; Col.
spliter.
unfold TS in H0.
spliter.
apply H0.
Col.
intro.
assert(¬ Parallelogram_strict A B D C ¬ Parallelogram_strict B A C D).
apply plgs_not_comm.
assumption.
spliter.
induction H1.
contradiction.
unfold Parallelogram_strict in H0.
unfold Parallelogram_flat in H1.
spliter.
unfold TS in H0.
spliter.
contradiction.
assert(¬ Parallelogram_flat A B D C ¬ Parallelogram_flat B A C D).
apply plgf_not_comm.
assumption.
assumption.
spliter.
split.
intro.
induction H3.
unfold Parallelogram_strict in H3.
unfold Parallelogram_flat in H0.
spliter.
unfold TS in H3.
spliter.
apply H3.
Col.
apply plgf_not_comm in H0.
spliter.
contradiction.
assumption.
intro.
induction H3.
unfold Parallelogram_strict in H3.
unfold Parallelogram_flat in H0.
spliter.
unfold TS in H3.
spliter.
contradiction.
contradiction.
Qed.

Lemma parallelogram_to_plg : A B C D, Parallelogram A B C D Plg A B C D.
Proof.
intros A B C D HPara.
destruct (plg_mid A B C D) as [M HM]; Col.
split; try ( M; Col).
elim HPara; clear HPara; intro HPara; try (apply plgs_diff in HPara; spliter; Col);
unfold Parallelogram_flat in HPara; spliter; Col.
Qed.

Lemma parallelogram_equiv_plg : A B C D, Parallelogram A B C D Plg A B C D.
Proof.
intros.
split.
apply parallelogram_to_plg.
apply plg_to_parallelogram.
Qed.

Lemma plg_conga : A B C D, A B A C B C Parallelogram A B C D CongA A B C C D A CongA B C D D A B.
intros.
assert(Cong A B C D Cong A D B C).
apply plg_cong.
assumption.
spliter.
assert(HH:= plg_mid A B C D H0).
ex_and HH M.
split.
apply cong3_conga; auto.
repeat split; Cong.
apply cong3_conga; auto.
intro.
subst D.
apply H.
eapply symmetric_point_uniqueness;
apply l7_2.
apply H5.
assumption.
repeat split; Cong.
Qed.

Lemma half_plgs :
  A B C D P Q M,
  Parallelogram_strict A B C D
  Midpoint P A B
  Midpoint Q C D
  Midpoint M A C
  Par P Q A D Midpoint M P Q Cong A D P Q.
Proof.
intros.
assert(HH:=H).
apply plgs_mid in HH.
ex_and HH M'.
assert(M=M').
eapply l7_17.
apply H2.
assumption.
subst M'.
clear H3.

prolong P M Q' P M.
assert(Midpoint M P Q').
split.
assumption.
Cong.
assert(Midpoint Q' C D).
eapply symmetry_preserves_midpoint.
apply H2.
apply H6.
apply H4.
apply H0.
assert(Q=Q').
eapply l7_17.
apply H1.
assumption.
subst Q'.
assert(HH:=H).
unfold Parallelogram_strict in HH.
spliter.

assert(Cong A P D Q).
eapply cong_cong_half_1.
apply H0.
apply l7_2.
apply H1.
Cong.

assert(Par A P Q D).
eapply par_col_par_2.
intro.
subst P.
apply is_midpoint_id in H0.
subst B.
induction H9.
unfold Par_strict in H0.
spliter.
tauto.
spliter.
tauto.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
apply col_permutation_5.
apply H0.
apply par_symmetry.
apply par_left_comm.
eapply par_col_par_2.
intro.
subst Q.
apply cong_identity in H11.
subst P.
apply is_midpoint_id in H0.
subst B.
induction H9.
unfold Par_strict in H0.
spliter.
tauto.
spliter.
tauto.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
apply col_permutation_2.
apply H1.
apply par_left_comm.
Par.

assert(Cong A D P Q Par A D P Q).
apply(os_cong_par_cong_par A P D Q).

unfold TS in H8.
assert(¬ Col B A C).
spliter.
assumption.
spliter.

assert(OS A D P B).
eapply out_one_side_1.
intro.
subst D.
apply H14.
Col.
intro.
assert(Col P B D).
eapply (col_transitivity_1 _ A).
intro.
subst P.
apply is_midpoint_id in H0.
subst B.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst D.
apply H14.
Col.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
Col.
Col.

assert(HH:=H).
apply plgs_permut in HH.
unfold Parallelogram_strict in HH.
spliter.
unfold TS in H18.
assert(¬ Col C B D).
spliter.
assumption.
spliter.
apply H22.
apply col_permutation_1.
eapply (col_transitivity_1 _ P).
intro.
subst P.
apply H22.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
Col.
Col.
Col.
Col.
unfold Midpoint in H0.
spliter.

repeat split.
intro.
subst P.
apply cong_symmetry in H11.
apply cong_identity in H11;

unfold TS in H8.
subst Q.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst D.
apply H14.
Col.
intro.
subst B.
apply cong_symmetry in H10.
apply cong_identity in H10;
unfold Par_strict in H12.
subst D.
apply H13.
Col.
left.
assumption.

assert(OS A D Q C).
eapply out_one_side_1.
intro.
subst D.
apply H14.
Col.
intro.
apply H14.
eapply (col_transitivity_1 _ Q).
intro.
subst Q.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst D.
apply H14.
Col.
Col.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
Col.
apply col_trivial_2;Col.

repeat split.
intro.
subst Q.
apply cong_identity in H11.
subst P.
unfold OS in H16.
ex_and H16 K.
unfold TS in H11.
spliter.
apply H11.
Col.
intro.
subst D.
apply cong_identity in H10.
subst B.
apply H14.
Col.

unfold Midpoint in H1.
spliter.
left.
Between.

assert(OS A D B C).

apply ts_cong_par_cong_par in H9.
spliter.

induction H18.
apply l12_6.
unfold Par_strict in ×.
spliter.
repeat split; auto; try apply all_coplanar.
intro.
apply H21.
ex_and H22 X.
X.
split; Col.
spliter.
apply False_ind.
apply H13.
Col.
repeat split; auto.
Cong.
eapply one_side_transitivity.
apply H16.
eapply one_side_transitivity.
apply H18.
apply one_side_symmetry.
assumption.
assumption.
Par.
spliter.
apply par_symmetry in H14.
split; auto.
Qed.

Lemma plgs_two_sides :
  A B C D,
 Parallelogram_strict A B C D
 TS A C B D TS B D A C.
Proof.
intros.
assert(HH:= plgs_mid A B C D H).
ex_and HH M.
unfold Parallelogram_strict in H.
spliter.
split.
assumption.

unfold TS.
assert(¬Col B A C).
unfold TS in H.
spliter.
Col.
assert(B D).
intro.
assert(HH:=one_side_reflexivity A C B H4).
apply l9_9 in H.
subst D.
contradiction.
unfold TS in H.
assert(¬ Col B A C).
spliter.
assumption.
spliter.
repeat split.
intro.
assert(Col M A B).
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
ColR.

apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ M).
intro.
subst M.
apply is_midpoint_id in H0.
subst C.
Col.
unfold Midpoint in H0.
spliter.
apply bet_col.
assumption.
Col.
intro.
assert(Col M B C).
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
ColR.
apply H6.
apply col_permutation_1.
eapply (col_transitivity_1 _ M).
intro.
subst M.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst C.
Col.
Col.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
Col.
M.
unfold Midpoint in ×.
spliter.
apply bet_col in H1.
split; Col.
Qed.

Lemma plgs_par_strict :
  A B C D,
  Parallelogram_strict A B C D
  Par_strict A B C D Par_strict A D B C.
Proof.
intros A B C D HPara.
destruct (plgs_mid A B C D) as [M [HMid1 HMid2]]; Col.
destruct HPara as [HTS [HCong HPar]].
assert(HAB : A B) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
assert(HAC : A D) by (intro; treat_equalities; unfold TS in HTS; spliter; Col).
unfold TS in HTS; spliter; split; try apply par_not_col_strict with C; Col.
assert (Par A D C B); Par; apply l12_17 with M; Midpoint.
Qed.

Lemma plgs_half_plgs_aux :
  A B C D P Q,
  Parallelogram_strict A B C D
  Midpoint P A B
  Midpoint Q C D
  Parallelogram_strict A P Q D.
Proof.
intros.
assert(HH:= H).
apply plgs_mid in HH.
ex_and HH M.
assert(HH:=half_plgs A B C D P Q M H H0 H1 H2).
spliter.

assert(HH:=H).
apply plgs_par_strict in HH.
spliter.

assert(HH:=par_cong_mid P Q A D H4 (cong_symmetry A D P Q H6)).
ex_and HH N.
induction H9.
spliter.
apply False_ind.
unfold Par_strict in H7.
spliter.
apply H13.
N.

assert(A P).
intro.
subst P.
apply l7_3 in H9.
subst N.
apply is_midpoint_id in H0.
subst B.
tauto.

assert(D Q).
intro.
subst Q.
apply l7_3 in H10.
subst N.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst D.
tauto.

unfold Midpoint in ×.
spliter.
split.
apply bet_col in H0.
apply bet_col in H9.
ColR.
apply bet_col in H1.
apply bet_col in H10.
ColR.

spliter.

assert(A P).
intro.
subst P.
apply is_midpoint_id in H0.
subst B.
unfold Par_strict in H7.
spliter.
tauto.

assert(D Q).
intro.
subst Q.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst D.
unfold Par_strict in H7.
spliter.
tauto.

eapply mid_plgs.
intro.
unfold Par_strict in H7.
spliter.
apply H16.
Q.
split.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
ColR.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
Col.
apply l7_2.
apply H10.
assumption.
Qed.

Lemma plgs_comm2 :
  A B C D,
  Parallelogram_strict A B C D
  Parallelogram_strict B A D C.
Proof.
intros.
assert(HH:= H).
apply plgs_two_sides in HH.
spliter.
unfold Parallelogram_strict in ×.
split.
assumption.
spliter.
split.
apply par_comm.
assumption.
Cong.
Qed.

Lemma plgf_comm2 :
  A B C D,
  Parallelogram_flat A B C D
  Parallelogram_flat B A D C.
Proof.
intros.
unfold Parallelogram_flat in ×.
spliter.
repeat split; Col.
Cong.
Cong.
induction H3.
right; assumption.
left; assumption.
Qed.

Lemma plg_comm2 :
  A B C D,
  Parallelogram A B C D
  Parallelogram B A D C.
Proof.
intros.
induction H.
left.
apply plgs_comm2.
assumption.
right.
apply plgf_comm2.
assumption.
Qed.

Lemma par_preserves_conga_ts :
  A B C D , Par A B C D TS B D A C CongA A B D C D B.
Proof.
intros.
assert(A C B D A B C D).
unfold Par in H.
unfold TS in H0.
assert(¬ Col A B D).
spliter.
assumption.
spliter.
induction H.
unfold Par_strict in H.
spliter.
repeat split; auto.
intro.
subst C.
apply H6.
A.
split; Col.
intro.
subst D.
Col.
spliter.
repeat split; auto.
intro.
subst C.
apply H2.
ex_and H3 T.
apply between_identity in H7.
subst T.
assumption.
intro.
subst D.
Col.
spliter.

assert(HH:=midpoint_existence B D).
ex_and HH M.
prolong A M C' A M.
assert(Midpoint M A C').
unfold Midpoint.
split.
assumption.
Cong.

assert(A C').
intro.
subst C'.
apply l7_3 in H8.
subst M.
unfold TS in H0.
spliter.
apply H0.
apply midpoint_bet in H5.
apply bet_col in H5.
Col.

assert(Parallelogram A B C' D).
apply (mid_plg A B C' D M).
right.
unfold TS in H0.
spliter.
assumption.
assumption.
assumption.

assert(Par A B C' D).
eapply midpoint_par.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
assumption.
spliter.
assumption.
apply H8.
assumption.

assert(¬Col D A B).
intro.
unfold TS in H0.
spliter.
apply H0.
Col.

assert(Col C' C D Col D C D).
apply (parallel_uniqueness A B C D C' D D); Col.
spliter.
clear H14.

assert(Out D C C').
unfold Out.
repeat split.
assumption.
intro.
subst C'.
unfold Par in H11.
induction H11;

spliter.
unfold Par_strict in H11.
spliter.
tauto.
tauto.
unfold Col in H13.
induction H13.
left.
Between.
induction H13.
apply False_ind.

assert(¬Col C' B D).
intro.
unfold Par in H11.
induction H11.
unfold Par_strict in H11.
spliter.
apply H17.
B.
split; Col.
spliter.
apply H12.
eapply (col_transitivity_1 _ C').
auto.
Col.
Col.

assert(TS B D A C').
unfold TS.
repeat split.
unfold TS in H0.
spliter.
assumption.
assumption.
M.
unfold Midpoint in ×.
spliter.
apply bet_col in H5.
apply bet_col in H6.
split; Col.

assert(TS B D C C').
unfold TS.
repeat split.
unfold TS in H0.
spliter.
assumption.
assumption.
D.
split.
Col.
assumption.
assert(OS B D C C').
unfold OS.
A.
split.
apply l9_2.
assumption.
apply l9_2.
assumption.
apply l9_9 in H16.
contradiction.
right.
assumption.
cut(CongA A B D C' D B).
intro.
eapply out_conga.
apply H15.
apply out_trivial.
apply out_trivial.
assumption.
apply out_trivial.
auto.
apply l6_6.
assumption.
apply out_trivial.
assumption.
apply plg_conga1; auto.
apply parallelogram_to_plg.
apply plg_comm2.
assumption.
Qed.

Lemma par_preserves_conga_os :
  A B C D P , Par A B C D Bet A D P D P OS A D B C CongA B A P C D P.
Proof.
intros.
assert(HH:= H2).
unfold OS in HH.
ex_and HH T.
unfold TS in ×.
spliter.

prolong C D C' C D.

assert(C' D).
intro.
subst C'.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst D.
apply H4.
Col.

assert(CongA B A D C' D A).
eapply par_preserves_conga_ts.
apply par_comm.
apply par_symmetry.
eapply (par_col_par_2 _ C).
auto.

apply bet_col in H9.
Col.
apply par_symmetry.
Par.
apply (l9_8_2 _ _ C).
unfold TS.
repeat split; auto.
intro.
apply H4.
apply bet_col in H9.
ColR.

D.
split.
Col.
assumption.
apply one_side_symmetry.
assumption.

assert(A B).
intro.
subst B.
apply H3.
Col.

assert(CongA B A D B A P).
assert(A D).
intro.
subst D.
Col.
eapply (out_conga B A D B A D).
apply conga_refl.
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold Out.
repeat split; auto.
intro.
subst P.
apply between_identity in H0.
contradiction.
apply conga_right_comm.

assert(CongA C D P C' D A).
eapply l11_14; auto.
intro.
subst D.
apply H4.
Col.
Between.
intro.
subst D.
Col.
eapply conga_trans.
apply conga_sym.
apply H14.
eapply conga_trans.
apply H12.
apply conga_sym.
apply conga_left_comm.
assumption.
Qed.

Lemma cong3_par2_par :
  A B C A' B' C', A C Cong_3 B A C B' A' C' Par B A B' A' Par B C B' C'
 Par A C A' C' ¬ Par_strict B B' A A' ¬Par_strict B B' C C'.
Proof.
intros.

assert(HH0:=par_distinct B A B' A' H1).
assert(HH1:=par_distinct B C B' C' H2).
spliter.

assert(HH:=midpoint_existence B B').
ex_and HH M.

prolong A M A'' A M.
prolong C M C'' C M.

assert(Midpoint M A A'').
split; Cong.
assert(Midpoint M C C'').
split; Cong.

assert(Par B A B' A'').
apply (midpoint_par _ _ _ _ M); assumption.

assert(Par B C B' C'').
apply (midpoint_par _ _ _ _ M); assumption.

assert(Par A C A'' C'').
apply (midpoint_par _ _ _ _ M);assumption.

assert(Par B' A' B' A'').
eapply par_trans.
apply par_symmetry.
apply H1.
assumption.

assert(Par B' C' B' C'').
eapply par_trans.
apply par_symmetry.
apply H2.
assumption.

assert(Col B' A' A'').
unfold Par in H17.
induction H17.
apply False_ind.
apply H17.
B'.
split; Col.
spliter.
Col.

assert(Col B' C' C'').
unfold Par in H18.
induction H18.
apply False_ind.
apply H18.
B'.
split; Col.
spliter.
Col.

assert(Cong B A B' A'').
eapply l7_13.
apply l7_2.
apply H7.
apply l7_2.
assumption.

assert(Cong B C B' C'').
eapply l7_13.
apply l7_2.
apply H7.
apply l7_2.
assumption.

unfold Cong_3 in H0.
spliter.

assert(A' = A'' Midpoint B' A' A'').
eapply l7_20.
Col.
eCong.

assert(C' = C'' Midpoint B' C' C'').
eapply l7_20.
Col.
eCong.

induction H25.

induction H26.
subst A''.
subst C''.
left.
assumption.

right; left.
intro.
apply H27.
M.
unfold Midpoint in ×.
spliter.
split.
apply bet_col in H7.
Col.
subst.
apply bet_col in H8.
Col.

induction H26.

subst C''.
clean_duplicated_hyps.
clean_trivial_hyps.

right; right.
intro.
apply H15.
M.
split.
unfold Midpoint in H7.
spliter.
apply bet_col in H7.
Col.
unfold Midpoint in H13.
spliter.
apply bet_col in H13.
Col.

assert(Par A' C' A'' C'').

apply(midpoint_par A' C' A'' C'' B').

intro.
subst C'.
assert(A'' = C'').
eapply l7_9.
apply l7_2.
apply H25.
apply l7_2.
assumption.
subst C''.
apply H.
eapply l7_9.
apply H12.
assumption.
apply H25.
apply H26.
left.
eapply par_trans.
apply H16.
Par.
Qed.

Lemma square_perp_rectangle : A B C D,
 Rectangle A B C D
 Perp A C B D
 Square A B C D.
Proof.
intros.
assert (Rhombus A B C D).
apply perp_rmb.
apply H. assumption.
apply Rhombus_Rectangle_Square;auto.
Qed.

Lemma plgs_half_plgs :
  A B C D P Q,
  Parallelogram_strict A B C D
  Midpoint P A B Midpoint Q C D
  Parallelogram_strict A P Q D Parallelogram_strict B P Q C.
Proof.
intros.
split.
eapply plgs_half_plgs_aux.
apply H.
assumption.
assumption.
apply plgs_comm2 in H.
eapply plgs_half_plgs_aux.
apply H.
Midpoint.
Midpoint.
Qed.

Lemma parallel_2_plg :
   A B C D,
  ¬ Col A B C
  Par A B C D
  Par A D B C
  Parallelogram_strict A B C D.
Proof.
intros.
assert (Cong A B C D Cong B C D A
        TS B D A C TS A C B D)
  by (apply l12_19;Par).
unfold Parallelogram_strict; intuition.
Qed.

Lemma par_2_plg :
   A B C D,
  ¬ Col A B C
  Par A B C D
  Par A D B C
  Parallelogram A B C D.
Proof.
intros.
assert (H2 := parallel_2_plg A B C D H H0 H1).
apply Parallelogram_strict_Parallelogram; assumption.
Qed.

Lemma parallelogram_strict_not_col_2 : A B C D,
 Parallelogram_strict A B C D
 ¬ Col B C D.
Proof.
intros.
apply plgs_permut in H.
apply parallelogram_strict_not_col in H.
Col.
Qed.

Lemma parallelogram_strict_not_col_3 : A B C D,
 Parallelogram_strict A B C D
 ¬ Col C D A.
Proof.
intros.
apply plgs_sym in H.
apply parallelogram_strict_not_col in H.
assumption.
Qed.

Lemma parallelogram_strict_not_col_4 : A B C D,
 Parallelogram_strict A B C D
 ¬ Col A B D.
Proof.
intros.
apply plgs_sym in H.
apply plgs_permut in H.
apply parallelogram_strict_not_col in H.
Col.
Qed.

Lemma plg_cong_1 : A B C D, Parallelogram A B C D Cong A B C D.
Proof.
intros.
apply plg_cong in H.
spliter.
assumption.
Qed.

Lemma plg_cong_2 : A B C D, Parallelogram A B C D Cong A D B C.
Proof.
intros.
apply plg_cong in H.
spliter.
assumption.
Qed.

Lemma plgs_cong_1 : A B C D, Parallelogram_strict A B C D Cong A B C D.
Proof.
intros.
apply plgs_cong in H.
spliter.
assumption.
Qed.

Lemma plgs_cong_2 : A B C D, Parallelogram_strict A B C D Cong A D B C.
Proof.
intros.
apply plgs_cong in H.
spliter.
assumption.
Qed.

Lemma Plg_perm :
   A B C D,
  Parallelogram A B C D
  Parallelogram A B C D Parallelogram B C D A Parallelogram C D A B Parallelogram D A B C
  Parallelogram A D C B Parallelogram D C B A Parallelogram C B A D Parallelogram B A D C.
Proof.
intros.
split; try assumption.
split; try (apply plg_permut; assumption).
split; try (do 2 apply plg_permut; assumption).
split; try (do 3 apply plg_permut; assumption).
split; try (apply plg_comm2; do 3 apply plg_permut; assumption).
split; try (apply plg_comm2; do 2 apply plg_permut; assumption).
split; try (apply plg_comm2; apply plg_permut; assumption).
apply plg_comm2; assumption.
Qed.

Lemma plg_not_comm_1 :
   A B C D : Tpoint,
  A B
  Parallelogram A B C D ¬ Parallelogram A B D C.
Proof.
intros.
assert (HNC := plg_not_comm A B C D H H0); spliter; assumption.
Qed.

Lemma plg_not_comm_2 :
   A B C D : Tpoint,
  A B
  Parallelogram A B C D ¬ Parallelogram B A C D.
Proof.
intros.
assert (HNC := plg_not_comm A B C D H H0); spliter; assumption.
Qed.

End Quadrilateral_inter_dec_1.

Ltac permutation_intro_in_hyps_aux :=
 repeat
 match goal with
 | H : Plg_tagged ?A ?B ?C ?D |- _apply Plg_tagged_Plg in H; apply Plg_perm in H; spliter
 | H : Par_tagged ?A ?B ?C ?D |- _apply Par_tagged_Par in H; apply Par_perm in H; spliter
 | H : Par_strict_tagged ?A ?B ?C ?D |- _apply Par_strict_tagged_Par_strict in H; apply Par_strict_perm in H; spliter
 | H : Perp_tagged ?A ?B ?C ?D |- _apply Perp_tagged_Perp in H; apply Perp_perm in H; spliter
 | H : Perp_in_tagged ?X ?A ?B ?C ?D |- _apply Perp_in_tagged_Perp_in in H; apply Perp_in_perm in H; spliter
 | H : Per_tagged ?A ?B ?C |- _apply Per_tagged_Per in H; apply Per_perm in H; spliter
 | H : Mid_tagged ?A ?B ?C |- _apply Mid_tagged_Mid in H; apply Mid_perm in H; spliter
 | H : NCol_tagged ?A ?B ?C |- _apply NCol_tagged_NCol in H; apply NCol_perm in H; spliter
 | H : Col_tagged ?A ?B ?C |- _apply Col_tagged_Col in H; apply Col_perm in H; spliter
 | H : Bet_tagged ?A ?B ?C |- _apply Bet_tagged_Bet in H; apply Bet_perm in H; spliter
 | H : Cong_tagged ?A ?B ?C ?D |- _apply Cong_tagged_Cong in H; apply Cong_perm in H; spliter
 | H : Diff_tagged ?A ?B |- _apply Diff_tagged_Diff in H; apply Diff_perm in H; spliter
 end.

Ltac permutation_intro_in_hyps := clean_reap_hyps; clean_trivial_hyps; tag_hyps; permutation_intro_in_hyps_aux.

Ltac assert_cols_aux :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)

      | H:Midpoint ?X1 ?X2 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := midpoint_col X2 X1 X3 H)

      | H:Out ?X1 ?X2 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := out_col X1 X2 X3 H)

      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id X1 X2 X3 H)
      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id_1 X1 X2 X3 H)
      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id_2 X1 X2 X3 H)
      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id_3 X1 X2 X3 H)
      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id_4 X1 X2 X3 H)
      | H:Par ?X1 ?X2 ?X1 ?X3 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := par_id_5 X1 X2 X3 H)

      | H:Par ?X1 ?X2 ?X3 ?X4, H2:Col ?X1 ?X2 ?X5, H3:Col ?X3 ?X4 ?X5 |- _
     not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := not_strict_par1 X1 X2 X3 X4 X5 H H2 H3)
 end.

Ltac assert_cols_perm := permutation_intro_in_hyps; assert_cols_aux; clean_reap_hyps.

Ltac not_exist_hyp_perm_cong A B C D := not_exist_hyp (Cong A B C D); not_exist_hyp (Cong A B D C);
                                        not_exist_hyp (Cong B A C D); not_exist_hyp (Cong B A D C);
                                        not_exist_hyp (Cong C D A B); not_exist_hyp (Cong C D B A);
                                        not_exist_hyp (Cong D C A B); not_exist_hyp (Cong D C B A).

Ltac assert_congs_1 :=
repeat
 match goal with
      | H:Midpoint ?X1 ?X2 ?X3 |- _
      let h := fresh in
      not_exist_hyp_perm_cong X1 X2 X1 X3;
      assert (h := midpoint_cong X2 X1 X3 H)

      | H1:Midpoint ?M1 ?A1 ?B1, H2:Midpoint ?M2 ?A2 ?B2, H3:Cong ?A1 ?B1 ?A2 ?B2 |- _
      let h := fresh in
      not_exist_hyp_perm_cong A1 M1 A2 M2;
      assert (h := cong_cong_half_1 A1 M1 B1 A2 M2 B2 H1 H2 H3)

      | H:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_cong X1 X2 X3 X4;
      assert (h := plg_cong_1 X1 X2 X3 X4 H)

      | H:Parallelogram_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_cong X1 X2 X3 X4;
      assert (h := plgs_cong_1 X1 X2 X3 X4 H)
  end.

Ltac assert_congs_2 :=
repeat
 match goal with
      | H1:Midpoint ?M1 ?A1 ?B1, H2:Midpoint ?M2 ?A2 ?B2, H3:Cong ?A1 ?B1 ?A2 ?B2 |- _
      let h := fresh in
      not_exist_hyp_perm_cong A1 M1 A2 M2;
      assert (h := cong_cong_half_2 A1 M1 B1 A2 M2 B2 H1 H2 H3)

      | H:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_cong X1 X4 X2 X3;
      assert (h := plg_cong_2 X1 X2 X3 X4 H);clean_reap_hyps

      | H:Parallelogram_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_cong X1 X4 X2 X3;
      assert (h := plgs_cong_2 X1 X2 X3 X4 H);clean_reap_hyps
  end.

Ltac assert_congs_perm := permutation_intro_in_hyps; assert_congs_1; assert_congs_2; clean_reap_hyps.

Ltac not_exist_hyp_perm_para A B C D := not_exist_hyp (Parallelogram A B C D); not_exist_hyp (Parallelogram B C D A);
                                        not_exist_hyp (Parallelogram C D A B); not_exist_hyp (Parallelogram D A B C);
                                        not_exist_hyp (Parallelogram A D C B); not_exist_hyp (Parallelogram D C B A);
                                        not_exist_hyp (Parallelogram C B A D); not_exist_hyp (Parallelogram B A D C).

Ltac not_exist_hyp_perm_para_s A B C D := not_exist_hyp (Parallelogram_strict A B C D);
                                          not_exist_hyp (Parallelogram_strict B C D A);
                                          not_exist_hyp (Parallelogram_strict C D A B);
                                          not_exist_hyp (Parallelogram_strict D A B C);
                                          not_exist_hyp (Parallelogram_strict A D C B);
                                          not_exist_hyp (Parallelogram_strict D C B A);
                                          not_exist_hyp (Parallelogram_strict C B A D);
                                          not_exist_hyp (Parallelogram_strict B A D C).

Ltac assert_paras_aux :=
repeat
 match goal with
      | H:Parallelogram_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_para X1 X2 X3 X4;
      assert (h := Parallelogram_strict_Parallelogram X1 X2 X3 X4 H)

      | H:Plg ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_para X1 X2 X3 X4;
      assert (h := plg_to_parallelogram X1 X2 X3 X4 H)

      | H:(¬ Col ?X1 ?X2 ?X3), H2:Par ?X1 ?X2 ?X3 ?X4, H3:Par ?X1 ?X4 ?X2 ?X3 |- _
      let h := fresh in
      not_exist_hyp_perm_para_s X1 X2 X3 X4;
      assert (h := parallel_2_plg X1 X2 X3 X4 H H2 H3)
  end.

Ltac assert_paras_perm := permutation_intro_in_hyps; assert_paras_aux; clean_reap_hyps.

Ltac not_exist_hyp_perm_npara A B C D := not_exist_hyp (¬Parallelogram A B C D); not_exist_hyp (¬Parallelogram B C D A);
                                         not_exist_hyp (¬Parallelogram C D A B); not_exist_hyp (¬Parallelogram D A B C);
                                         not_exist_hyp (¬Parallelogram A D C B); not_exist_hyp (¬Parallelogram D C B A);
                                         not_exist_hyp (¬Parallelogram C B A D); not_exist_hyp (¬Parallelogram B A D C).

Ltac assert_nparas_1 :=
 repeat
 match goal with
      | H:(?X1?X2), H2:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_npara X1 X2 X4 X3;
      assert (h := plg_not_comm_1 X1 X2 X3 X4 H H2)
  end.

Ltac assert_nparas_2 :=
 repeat
 match goal with
      | H:(?X1?X2), H2:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_npara X2 X1 X3 X4;
      assert (h := plg_not_comm_2 X1 X2 X3 X4 H H2)
  end.

Ltac assert_nparas_perm := permutation_intro_in_hyps; assert_nparas_1; assert_nparas_2; clean_reap_hyps.

Ltac diag_plg_intersection M A B C D H :=
 let T := fresh in assert(T:= plg_mid A B C D H);
 ex_and T M.

Tactic Notation "Name" ident(M) "the" "intersection" "of" "the" "diagonals" "(" ident(A) ident(C) ")" "and" "(" ident(B) ident(D) ")" "of" "the" "parallelogram" ident(H) :=
 diag_plg_intersection M A B C D H.

Ltac assert_diffs :=
repeat
 match goal with
      | H:(¬Col ?X1 ?X2 ?X3) |- _
      let h := fresh in
      not_exist_hyp3 X1 X2 X1 X3 X2 X3;
      assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps

      | H:(¬Bet ?X1 ?X2 ?X3) |- _
      let h := fresh in
      not_exist_hyp2 X1 X2 X2 X3;
      assert (h := not_bet_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?A ?B |-_
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq12__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B ?A |-_
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq21__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B ?C |-_
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq23__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?C ?B |-_
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq32__neq A B C H H2);clean_reap_hyps

      | H:Cong ?A ?B ?C ?D, H2 : ?A ?B |-_
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?B ?A |-_
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?C ?D |-_
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?D ?C |-_
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps

      | H:(Parallelogram_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X1 X2 X3);
      assert (HN := parallelogram_strict_not_col X1 X2 X3 X4 H)
      | H:(Parallelogram_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X2 X3 X4);
      assert (HN := parallelogram_strict_not_col_2 X1 X2 X3 X4 H)
      | H:(Parallelogram_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X3 X4 X1);
      assert (HN := parallelogram_strict_not_col_3 X1 X2 X3 X4 H)
      | H:(Parallelogram_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X1 X2 X4);
      assert (HN := parallelogram_strict_not_col_4 X1 X2 X3 X4 H)

      | H:Midpoint ?I ?A ?B, H2 : ?A?B |- _
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B?A |- _
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I?A |- _
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?A?I |- _
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I?B |- _
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B?I |- _
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Perp ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_distinct A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Perp_at ?X ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_in_distinct X A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Out ?A ?B ?C |- _
      let T:= fresh in (not_exist_hyp2 A B A C);
       assert (T:= out_distinct A B C H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= conga_diff1 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _
      let T:= fresh in (not_exist_hyp_comm B C);
        assert (T:= conga_diff2 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _
      let T:= fresh in (not_exist_hyp_comm A' B');
        assert (T:= conga_diff45 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _
      let T:= fresh in (not_exist_hyp_comm B' C');
        assert (T:= conga_diff56 A B C A' B' C' H);clean_reap_hyps

      | H:LeA ?A ?B ?C ?D ?E ?F |- _
      let h := fresh in
      not_exist_hyp4 A B B C D E E F;
      assert (h := lea_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
      | H:LtA ?A ?B ?C ?D ?E ?F |- _
      let h := fresh in
      not_exist_hyp4 A B B C D E E F;
      assert (h := lta_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
      | H:(Acute ?A ?B ?C) |- _
      let h := fresh in
      not_exist_hyp3 A B A C B C;
      assert (h := acute_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps
      | H:(Obtuse ?A ?B ?C) |- _
      let h := fresh in
      not_exist_hyp3 A B A C B C;
      assert (h := obtuse_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps

      | H:(Par_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X1 X2 X3);
      assert (HN := par_strict_not_col_1 X1 X2 X3 X4 H)
      | H:(Par_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X2 X3 X4);
      assert (HN := par_strict_not_col_2 X1 X2 X3 X4 H)
      | H:(Par_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X3 X4 X1);
      assert (HN := par_strict_not_col_3 X1 X2 X3 X4 H)
      | H:(Par_strict ?X1 ?X2 ?X3 ?X4) |- _
      let HN := fresh in
      not_exist_hyp (¬Col X1 X2 X4);
      assert (HN := par_strict_not_col_4 X1 X2 X3 X4 H)


   | H:Par_strict ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= par_strict_distinct A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Par ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= par_distincts A B C D H);decompose [and] T;clear T;clean_reap_hyps
      | H:Perp ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_distinct A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Perp_at ?X ?A ?B ?C ?D |- _
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_in_distinct X A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Out ?A ?B ?C |- _
      let T:= fresh in (not_exist_hyp2 A B A C);
       assert (T:= out_distinct A B C H);
       decompose [and] T;clear T;clean_reap_hyps
 end.

Hint Resolve parallelogram_strict_not_col
             parallelogram_strict_not_col_2
             parallelogram_strict_not_col_3
             parallelogram_strict_not_col_4 : Col.

Section Quadrilateral_inter_dec_2.

Context `{TE:Tarski_2D_euclidean}.

Lemma parallelogram_strict_midpoint : A B C D I,
  Parallelogram_strict A B C D
  Col I A C
  Col I B D
  Midpoint I A C Midpoint I B D.
Proof.
intros.
assert (T:=Parallelogram_strict_Parallelogram A B C D H).
assert (HpF := plg_mid A B C D T).
elim HpF; intros I' HI;spliter;clear HpF.
assert (H01 : Col A C I).
 Col.
assert (H02 : Col D B I).
 Col.
assert (H03 : ¬Col A D C).
 apply parallelogram_strict_not_col_3 in H.
 Col.
unfold Parallelogram_strict in H.
decompose [and] H.
assert (H8 := two_sides_not_col A C B D H4).
assert (MDB:DB).
 assert (Col A I' C).
  assert (H9 := midpoint_bet A I' C H2).
  assert (H10 := bet_col A I' C H9).
  assumption.
 assert (H11 : ¬ Col A C D).
  Col.
 assert (H12 := l7_2 I' B D H3).
 assert (H13 : Col A C I').
  Col.
 apply (Ch08_orthogonality.distinct A C I' D B H11 H13 H12).
assert (H11 : Col D B I').
 assert (H14 := midpoint_bet B I' D H3).
 assert (H15 := bet_col B I' D H14).
 Col.
assert (H12 : Col A C I').
 assert (H14 := midpoint_bet A I' C H2).
 assert (H15 := bet_col A I' C H14).
 Col.
apply not_col_permutation_5 in H03.
assert (H13 := l6_21 A C D B I I' H03 MDB H01 H12 H02 H11).
split.
 rewrite H13;assumption.
 subst;assumption.
Qed.

Lemma rmb_perp :
  A B C D,
  A C B D
  Rhombus A B C D
  Perp A C B D.
Proof.
intros.
assert(HH:= H1).
unfold Rhombus in HH.
spliter.
apply plg_to_parallelogram in H2.
apply plg_mid in H2.
ex_and H2 M.
assert(HH:= H1).
eapply (rmb_per _ _ _ _ M) in HH.
apply per_perp_in in HH.

apply perp_in_perp_bis in HH.
induction HH.
apply perp_not_eq_1 in H5.
tauto.
unfold Midpoint in ×.
spliter.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
auto.
apply perp_left_comm.
apply perp_sym.
apply H5.
apply bet_col in H4.
Col.
apply bet_col in H2.
Col.
intro.
subst M.
apply is_midpoint_id in H2.
contradiction.
intro.
subst M.
apply l7_2 in H4.
apply is_midpoint_id in H4.
subst D.
tauto.
assumption.
Qed.

Lemma par_perp_perp : A B C D P Q, Par A B C D Perp A B P Q Perp C D P Q.
Proof.
intros.
apply universal_posidonius_postulate__perpendicular_transversal_postulate with A B;
try assumption; apply playfair__universal_posidonius_postulate.
unfold playfair_s_postulate; apply parallel_uniqueness.
Qed.

Lemma par_perp_2_par : A B C D E F G H,
  Par A B C D
  Perp A B E F
  Perp C D G H
  Par E F G H.
Proof.
intros.
apply par_perp_perp_implies_par_perp_2_par with A B C D; auto.
apply universal_posidonius_postulate__perpendicular_transversal_postulate.
apply playfair__universal_posidonius_postulate.
unfold playfair_s_postulate; apply parallel_uniqueness.
Qed.

Lemma rect_permut : A B C D, Rectangle A B C D Rectangle B C D A.
intros.
unfold Rectangle in ×.
spliter.
split.
apply plg_to_parallelogram in H.
apply plg_permut in H.
apply parallelogram_to_plg in H.
assumption.
Cong.
Qed.

Lemma rect_comm2 : A B C D, Rectangle A B C D Rectangle B A D C.
intros.
unfold Rectangle in ×.
spliter.
apply plg_to_parallelogram in H.

apply plg_comm2 in H.
split.
apply parallelogram_to_plg.
assumption.
Cong.
Qed.

Lemma rect_per1 : A B C D, Rectangle A B C D Per B A D.
intros.
unfold Rectangle in H.
spliter.

assert(HH:= midpoint_existence A B).
ex_and HH P.
assert(HH:= midpoint_existence C D).
ex_and HH Q.
assert(HH:=H).
unfold Plg in HH.
spliter.
ex_and H4 M.
apply plg_to_parallelogram in H.
induction H.

assert(HH:=half_plgs A B C D P Q M H H1 H2 H4).
spliter.
assert(Per A P Q).
eapply (per_col _ _ M).
intro.
subst M.
apply is_midpoint_id in H7.
subst Q.
apply cong_identity in H8.
subst D.
assert(B = C).
eapply symmetric_point_uniqueness.
apply l7_2.
apply H5.
Midpoint.
subst C.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.
apply H9.
Col.
apply l8_2.
unfold Per.
B.
split.
assumption.
eapply (cong_cong_half_1 _ M _ _ M) in H0.
Cong.
assumption.
assumption.
unfold Midpoint in H7.
spliter.
apply bet_col.
assumption.

assert(A B).
intro.
subst B.
apply l7_3 in H1.
subst P.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.
apply H.
Col.

assert(A P).
intro.
subst P.
apply is_midpoint_id in H1.
contradiction.

apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.

apply perp_sym.
apply perp_left_comm.
eapply par_perp_perp.
apply H6.
apply per_perp_in in H9.
apply perp_in_perp_bis in H9.
induction H9.
apply perp_not_eq_1 in H9.
tauto.
apply perp_sym.
eapply perp_col.
assumption.
apply H9.
unfold Midpoint in H1.
spliter.
apply bet_col.
assumption.
assumption.

induction H6.
unfold Par_strict in H6.
spliter.
assumption.
spliter.
assumption.
unfold Parallelogram_flat in H.
spliter.

assert(A = B C = D A = D C = B).
apply(midpoint_cong_uniqueness A C B D M).
Col.
split; assumption.
assumption.
induction H10.
spliter.
subst B.
apply l8_2.
apply l8_5.
spliter.
subst D.
apply l8_5.
Qed.

Lemma rect_per2 : A B C D, Rectangle A B C D Per A B C.
intros.
apply rect_comm2 in H.
eapply rect_per1.
apply H.
Qed.

Lemma rect_per3 : A B C D, Rectangle A B C D Per B C D.
intros.
apply rect_permut in H.
apply rect_comm2 in H.
eapply rect_per1.
apply H.
Qed.

Lemma rect_per4 : A B C D, Rectangle A B C D Per A D C.
intros.
apply rect_comm2 in H.
eapply rect_per2.
apply rect_permut.
apply H.
Qed.

Lemma plg_per_rect1 : A B C D, Plg A B C D Per D A B Rectangle A B C D.
intros.

assert(HH:= midpoint_existence A B).
ex_and HH P.
assert(HH:= midpoint_existence C D).
ex_and HH Q.
assert(HH:=H).
unfold Plg in HH.
spliter.
ex_and H4 M.
apply plg_to_parallelogram in H.
induction H.

assert(HH:=half_plgs A B C D P Q M H H1 H2 H4).
spliter.

assert(A D P Q).
induction H6.
unfold Par_strict in H6.
spliter.
unfold Par in H6.
split; assumption.
spliter.
split; assumption.
spliter.

assert(A B).
intro.
subst B.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.
apply H.
Col.
assert(A P).
intro.
subst P.
apply is_midpoint_id in H1.
contradiction.

assert(Perp P Q A B).
apply (par_perp_perp A D P Q A B).
Par.
apply per_perp_in in H0.
apply perp_in_comm in H0.
apply perp_in_perp_bis in H0.
induction H0.
apply perp_right_comm.
assumption.
apply perp_not_eq_1 in H0.
tauto.
auto.
assumption.

assert(Perp P M A B).
eapply perp_col.
intro.
subst M.
apply is_midpoint_id in H7.
contradiction.
apply H13.
unfold Midpoint in H7.
spliter.
apply bet_col in H7.
Col.

assert(Perp A P P M).
eapply perp_col.
assumption.
apply perp_sym.
apply H14.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.
Col.

assert(Per A P M).
apply perp_comm in H15.
apply perp_perp_in in H15.
apply perp_in_comm in H15.
apply perp_in_per in H15.
assumption.

unfold Rectangle.
split.
apply parallelogram_to_plg .
left.
assumption.

apply l8_2 in H16.
unfold Per in H16.
ex_and H16 B'.
assert(B = B').
eapply symmetric_point_uniqueness.
apply H1.
assumption.
subst B'.

unfold Midpoint in H4.
spliter.
unfold Midpoint in H5.
spliter.
eapply l2_11.
apply H4.
apply H5.
Cong.
eCong.

unfold Rectangle.
split.
apply parallelogram_to_plg.
right.
assumption.

unfold Parallelogram_flat in H.
spliter.

assert(D = A B = A).
apply (l8_9 D A B).
assumption.
Col.
induction H10.
subst D.
apply cong_symmetry in H8.
apply cong_identity in H8.
subst C.
Cong.
subst B.
apply cong_symmetry in H7.
apply cong_identity in H7.
subst D.
Cong.
Qed.

Lemma plg_per_rect2 : A B C D, Plg A B C D Per C B A Rectangle A B C D.
intros.
apply rect_comm2.
apply plg_per_rect1.
apply parallelogram_to_plg.
apply plg_to_parallelogram in H.
apply plg_comm2.
assumption.
assumption.
Qed.

Lemma plg_per_rect3 : A B C D, Plg A B C D Per A D C Rectangle A B C D.
intros.
apply rect_permut.
apply plg_per_rect1.
apply parallelogram_to_plg.
apply plg_to_parallelogram in H.
apply plg_permut.
apply plg_sym.
assumption.
apply l8_2.
assumption.
Qed.

Lemma plg_per_rect4 : A B C D, Plg A B C D Per B C D Rectangle A B C D.
intros.
apply rect_comm2.
apply plg_per_rect3.
apply parallelogram_to_plg.
apply plg_to_parallelogram in H.
apply plg_comm2.
assumption.
assumption.
Qed.

Lemma plg_per_rect : A B C D, Plg A B C D (Per D A B Per C B A Per A D C Per B C D) Rectangle A B C D.
intros.
induction H0.
apply plg_per_rect1; assumption.
induction H0.
apply plg_per_rect2; assumption.
induction H0.
apply plg_per_rect3; assumption.
apply plg_per_rect4; assumption.
Qed.

Lemma rect_per : A B C D, Rectangle A B C D Per B A D Per A B C Per B C D Per A D C.
intros.
repeat split.
apply (rect_per1 A B C D); assumption.
apply (rect_per2 A B C D); assumption.
apply (rect_per3 A B C D); assumption.
apply (rect_per4 A B C D); assumption.
Qed.

Lemma plgf_rect_id : A B C D, Parallelogram_flat A B C D Rectangle A B C D A = D B = C A = B D = C.
intros.
unfold Parallelogram_flat in H.
spliter.
assert(Per B A D Per A B C Per B C D Per A D C).

apply rect_per.
assumption.
spliter.

assert(HH:=l8_9 A B C H6 H).
induction HH.
right.
subst B.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst D.
split; reflexivity.
left.
subst B.
apply cong_identity in H3.
subst D.
split; reflexivity.
Qed.

Lemma perp_3_perp :
  A B C D,
  Perp A B B C
  Perp B C C D
  Perp C D D A
  Perp D A A B.
Proof.
intros.
assert (Par A B C D).
  (apply (l12_9 A B C D B C); auto using perp_sym).
assert (Perp A B D A)
 by (apply (par_perp_perp C D A B D A);Perp;apply par_symmetry;auto).
auto using perp_sym, perp_left_comm.
Qed.

Lemma perp_3_rect :
  A B C D,
  ¬ Col A B C
  Perp A B B C
  Perp B C C D
  Perp C D D A
  Rectangle A B C D.
Proof.
intros.
assert (Par A B C D)
 by (apply (l12_9 A B C D B C);Perp).
assert (Perp D A A B)
 by (eapply perp_3_perp;eauto).
assert (Par A D B C)
 by (apply (l12_9 A D B C A B);Perp).
assert (Parallelogram_strict A B C D)
 by (apply (parallel_2_plg); auto).
apply plg_per_rect1.
apply parallelogram_to_plg.
apply Parallelogram_strict_Parallelogram.
assumption.
Perp.
Qed.

Lemma conga_to_par_ts : A B C D , TS B D A C CongA A B D C D B Par A B C D.
intros.

assert(A C B D A B C D).
unfold CongA in H0.
unfold TS in H.
spliter.
repeat split; auto.
intro.
subst C.
ex_and H6 T.
apply between_identity in H7.
subst T.
contradiction.
spliter.

assert(HH:=midpoint_existence B D).
ex_and HH M.
prolong A M C' A M.

assert(Midpoint M A C').
unfold Midpoint.
split.
assumption.
Cong.

assert(Par A B C' D).
unfold Par.
left.
eapply midpoint_par_strict.
assumption.
unfold TS in H.
spliter.
assumption.
apply H8.
assumption.

assert(Plg A B C' D).
unfold Plg.
split.
right.
assumption.
M.
split; assumption.

assert(HH:= plg_to_parallelogram A B C' D H10).
apply plg_comm2 in HH.
apply parallelogram_to_plg in HH.
apply plg_conga1 in HH.

assert(CongA C D B C' D B).
eapply conga_trans.
apply conga_sym.
apply H0.
assumption.

apply conga_comm in H11.

apply l11_22_aux in H11.
induction H11.

assert(Par A B C' D).
eapply midpoint_par.
assumption.
apply H8.
assumption.
apply par_symmetry.
apply par_left_comm.
eapply par_col_par_2.
auto.
apply out_col in H11.
apply col_permutation_5.
apply H11.
apply par_symmetry.
Par.

assert(TS B D A C').
unfold TS in H.
spliter.
unfold TS.
repeat split; auto.

intro.
apply H.
unfold Midpoint in H5.
spliter.
apply bet_col in H5.
apply bet_col in H6.
assert(Col B C' M).
ColR.
assert(Col A C' M).
ColR.
assert(Col D C' M).
ColR.
eapply (col3 M C').
intro.
subst C'.
apply l7_2 in H8.
apply is_midpoint_id in H8.
subst M.
apply H.
Col.
Col.
Col.
Col.
M.
split.
unfold Midpoint in H5.
spliter.
apply bet_col in H5.
Col.
assumption.
assert(OS B D A C).
eapply l9_8_1.
apply H12.
assumption.
apply l9_9 in H.
contradiction.
auto.
auto.
Qed.

Lemma conga_to_par_os : A B C D P , Bet A D P D P OS A D B C CongA B A P C D P
                                            Par A B C D.

intros.
assert(HH:= H1).
unfold OS in HH.
ex_and HH T.
unfold TS in ×.
spliter.

assert(HH:=H2).
unfold CongA in HH.
spliter.
clear H13.

prolong C D C' C D.

assert(CongA C D P C' D A).
eapply l11_14; auto.
intro.
subst C'.
apply cong_symmetry in H14.
apply cong_identity in H14.
contradiction.
Between.
intro; subst D; Col.
assert(CongA B A D B A P).
assert(AD).
intro; subst D; Col.
eapply (out_conga B A D B A D); try (apply out_trivial; auto).
apply conga_refl; auto.
unfold Out.
repeat split; auto.

assert(CongA B A D C' D A).
eapply conga_trans.
apply H16.
eapply conga_trans.
apply H2.
assumption.
apply par_left_comm.

assert(Par B A C' D).

eapply conga_to_par_ts.

assert(TS A D C C').
unfold TS.
repeat split; auto.
intro.
apply H4.
apply col_permutation_1.
eapply (col_transitivity_1 _ C').
intro.
subst C'.
apply cong_symmetry in H14.
apply cong_identity in H14.
contradiction.
apply bet_col in H13.
Col.
Col.
D.
split; Col.
eapply l9_8_2.
apply H18.
apply one_side_symmetry.
assumption.
assumption.
apply par_symmetry.
apply par_comm.
eapply par_col_par_2.
auto.
apply bet_col in H13.
apply col_permutation_1.
apply H13.
apply par_symmetry.
apply par_comm.
assumption.
Qed.

Lemma plg_par : A B C D, A B B C Parallelogram A B C D Par A B C D Par A D B C.
Proof.
intros.
assert(HH:= H1).
apply plg_mid in HH.
ex_and HH M.

assert(HH:=midpoint_par A B C D M H H2 H3).
apply l7_2 in H2.
assert(HH1:=midpoint_par B C D A M H0 H3 H2).
split.
assumption.
apply par_symmetry.
Par.
Qed.

Lemma plg_par_1 : A B C D, A B B C Parallelogram A B C D Par A B C D.
Proof with finish.
intros.
assert (HPar := plg_par A B C D H H0 H1); spliter...
Qed.

Lemma plg_par_2 : A B C D, A B B C Parallelogram A B C D Par A D B C.
Proof with finish.
intros.
assert (HPar := plg_par A B C D H H0 H1); spliter...
Qed.

Lemma plgs_pars_1: A B C D : Tpoint, Parallelogram_strict A B C D Par_strict A B C D.
Proof with finish.
intros.
assert (HPar := plgs_par_strict A B C D H); spliter...
Qed.

Lemma plgs_pars_2: A B C D : Tpoint, Parallelogram_strict A B C D Par_strict A D B C.
Proof with finish.
intros.
assert (HPar := plgs_par_strict A B C D H); spliter...
Qed.

End Quadrilateral_inter_dec_2.

Ltac not_exist_hyp_perm_par A B C D := not_exist_hyp (Par A B C D); not_exist_hyp (Par A B D C);
                                       not_exist_hyp (Par B A C D); not_exist_hyp (Par B A D C);
                                       not_exist_hyp (Par C D A B); not_exist_hyp (Par C D B A);
                                       not_exist_hyp (Par D C A B); not_exist_hyp (Par D C B A).

Ltac not_exist_hyp_perm_pars A B C D := not_exist_hyp (Par_strict A B C D); not_exist_hyp (Par_strict A B D C);
                                        not_exist_hyp (Par_strict B A C D); not_exist_hyp (Par_strict B A D C);
                                        not_exist_hyp (Par_strict C D A B); not_exist_hyp (Par_strict C D B A);
                                        not_exist_hyp (Par_strict D C A B); not_exist_hyp (Par_strict D C B A).

Ltac assert_pars_1 :=
 repeat
 match goal with
      | H:Par_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_par X1 X2 X3 X4;
      assert (h := par_strict_par X1 X2 X3 X4 H)

      | H:Par ?X1 ?X2 ?X3 ?X4, H2:Col ?X1 ?X2 ?X5, H3:(¬Col ?X3 ?X4 ?X5) |- _
      let h := fresh in
      not_exist_hyp_perm_pars X1 X2 X3 X4;
      assert (h := par_not_col_strict X1 X2 X3 X4 X5 H H2 H3)

      | H: ?X1 ?X2, H2:?X2 ?X3, H3:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_par X1 X2 X3 X4;
      assert (h := plg_par_1 X1 X2 X3 X4 H H2 H3)

      | H:Parallelogram_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_pars X1 X2 X3 X4;
      assert (h := plgs_pars_1 X1 X2 X3 X4 H)
  end.

Ltac assert_pars_2 :=
 repeat
 match goal with
      | H: ?X1 ?X2, H2:?X2 ?X3, H3:Parallelogram ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_par X1 X4 X2 X3;
      assert (h := plg_par_2 X1 X2 X3 X4 H H2 H3)

      | H:Parallelogram_strict ?X1 ?X2 ?X3 ?X4 |- _
      let h := fresh in
      not_exist_hyp_perm_pars X1 X4 X2 X3;
      assert (h := plgs_pars_2 X1 X2 X3 X4 H)
  end.

Ltac assert_pars_perm := permutation_intro_in_hyps; assert_pars_1; assert_pars_2; clean_reap_hyps.

Section Quadrilateral_inter_dec_3.

Context `{TE:Tarski_2D_euclidean}.

Lemma par_cong_cong : A B C D, Par A B C D Cong A B C D Cong A C B D Cong A D B C.
intros.

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H0.
apply cong_identity in H0.
subst D.
left.
Cong.

induction(eq_dec_points A D).
subst D.

assert(B = C Midpoint A B C).
eapply l7_20.
unfold Par in H.
induction H.
apply False_ind.
unfold Par_strict in H.
spliter.
apply H4.
A.
split; Col.
spliter.
Col.
Cong.
induction H2.
subst C.
left.
Cong.
unfold Midpoint in H2.
spliter.
left.
Cong.

assert(HH:=par_cong_mid A B C D H H0).
ex_and HH M.
induction H3.
spliter.
right.

assert(HH:=mid_par_cong A B C D M H1 H2 H3 H4).
spliter.
Cong.

induction(eq_dec_points A C).
subst C.
assert(B = D Midpoint A B D).
eapply l7_20.
unfold Par in H.
induction H.
apply False_ind.
unfold Par_strict in H.
spliter.
apply H7.
A.
split; Col.
spliter.
Col.
Cong.
induction H4.
subst D.
right.
Cong.
unfold Midpoint in H4.
spliter.
right.
Cong.

left.
spliter.
assert(HH:=mid_par_cong A B D C M H1 H4 H3 H5).
spliter.
Cong.
Qed.

Lemma col_cong_cong : A B C D, Col A B C Col A B D Cong A B C D Cong A C B D Cong A D B C.
intros.

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
left.
Cong.

induction(eq_dec_points C D).
subst D.
apply cong_identity in H1.
subst B.
right.
Cong.

apply par_cong_cong.
right.
repeat split; Col; ColR.
assumption.
Qed.

Lemma par_cong_plg :
   A B C D, Par A B C D Cong A B C D Plg A B C D Plg A B D C.
Proof.
intros A B C D HPar HCong.
destruct (par_cong_mid A B C D) as [M HM]; Col.
elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2].

  {
  left; split; try ( M; Col).
  elim (eq_dec_points A C); intro HAC; treat_equalities; Col; right;
  intro; treat_equalities; apply par_distincts in HPar; spliter; Col.
  }

  {
  right; split; try ( M; Col).
  elim (eq_dec_points A D); intro HAD; treat_equalities; Col; right;
  intro; treat_equalities; apply par_distincts in HPar; spliter; Col.
  }
Qed.

Lemma par_cong_plg_2 :
   A B C D,
  Par A B C D
  Cong A B C D
  Parallelogram A B C D Parallelogram A B D C.
Proof.
intros.
assert (HElim : Plg A B C D Plg A B D C)
  by (apply par_cong_plg; assumption).
elim HElim; intro.

  left; apply plg_to_parallelogram; assumption.

  right; apply plg_to_parallelogram; assumption.
Qed.

Lemma par_cong3_rect : A B C D, A C B D Par A B C D Cong A B C D Cong A D B C Cong A C B D Rectangle A B C D Rectangle A B D C.
intros.
unfold Par in H0.
induction H0.

assert(HH:=par_strict_cong_mid1 A B C D H0 H1).

induction HH.
spliter.
left.
unfold Rectangle.
split; auto.
unfold Plg.
split; auto.
spliter.
ex_and H5 M.

right.
unfold Rectangle.
split; auto.
unfold Plg.
split; auto.

left.
intro.
subst D.
unfold Par_strict in H0.
spliter.
apply H9.
A.
split; Col.
M.
split; auto.

spliter.
left.
unfold Rectangle.
split; auto.

apply parallelogram_to_plg.
unfold Parallelogram.
right.
unfold Parallelogram_flat.

induction(eq_dec_points C D).
subst D.
apply cong_identity in H1.
subst B.
repeat split; Col; Cong.
repeat split; Col; Cong; ColR.
Qed.

Lemma pars_par_pars : A B C D, Par_strict A B C D Par A D B C Par_strict A D B C.
intros.
induction H0.
assumption.
spliter.
repeat split; try assumption; try apply all_coplanar.
intro.
ex_and H4 X.
unfold Par_strict in H.
spliter.
apply H8.
C.
split; Col.
Qed.

Lemma pars_par_plg : A B C D, Par_strict A B C D Par A D B C Plg A B C D.
intros.
assert(Par_strict A D B C).
apply pars_par_pars; auto.

assert(Par A B C D).
left.
assumption.

assert(A B C D A D B C).
apply par_distinct in H0.
apply par_distinct in H2.
spliter.
auto.
spliter.

assert(A C).
intro.
subst C.
unfold Par_strict in H.
spliter.
apply H9.
A.
split; Col.

assert(B D).
intro.
subst D.
unfold Par_strict in H.
spliter.
apply H10.
B.
split; Col.

unfold Plg.
split.

left.
assumption.

assert(HH:=midpoint_existence A C).
ex_and HH M.
M.
split.
assumption.
prolong B M D' B M.
assert(Midpoint M B D').
unfold Midpoint.
split; auto.
Cong.
assert(Plg A B C D').
unfold Plg.
repeat split.
induction H.
left.

assumption.

M.
split; auto.

assert(Parallelogram A B C D').
apply plg_to_parallelogram.
assumption.
assert(HH:=plg_par A B C D' H3 H6 H14).
spliter.

assert(¬Col C A B).
intro.
unfold Par_strict in H.
spliter.
apply H20.
C.
split; Col.

assert(Col C C D Col D' C D).

apply (parallel_uniqueness A B C D C D' C H2).
Col.
assumption.
Col.
spliter.

assert(A D').
intro.
subst D'.
unfold Par_strict in H1.
spliter.
apply H22.
C.
split; Col.

assert(HH:=mid_par_cong A B C D' M H3 H20 H9 H12).
spliter.

assert(Col A A D Col D' A D).
apply (parallel_uniqueness B C A D A D' A).

Par.
Col.
apply par_left_comm.
Par.
Col.
spliter.

assert(D = D').

eapply (l6_21 A D C D D D'); Col.
intro.
unfold Par_strict in H.
spliter.
apply H30.
A.
split; Col.
subst D'.
assumption.
Qed.

Lemma not_par_pars_not_cong : O A B A' B', Out O A B Out O A' B' Par_strict A A' B B' ¬Cong A A' B B'.
intros.
intro.

assert(A B).
intro.
subst B.
unfold Par_strict in H1.
spliter.
apply H5.
A.
split; Col.

assert(A' B').
intro.
subst B'.
unfold Par_strict in H1.
spliter.
apply H6.
A'.
split; Col.

assert(O A).
unfold Out in H.
spliter.
auto.

assert(O A').
unfold Out in H0.
spliter.
auto.

assert(¬Col O A A').
intro.
apply out_col in H.
apply out_col in H0.
assert(Col O B A').
ColR.
unfold Par_strict in H1.
spliter.
apply H11.
O.
split.
assumption.
ColR.

assert(OS A B A' B').

eapply(out_one_side_1 _ _ _ _ O).
assumption.
intro.
apply H7.
apply out_col in H.
apply out_col in H0.
ColR.
apply out_col in H.
Col.
assumption.

assert(Par A A' B B').
left.
assumption.

assert(HH:=os_cong_par_cong_par A A' B B' H8 H2 H9).
spliter.
unfold Par in H11.
induction H11.
unfold Par_strict in H11.
spliter.
apply H14.
O.
split.
apply out_col in H.
assumption.
apply out_col in H0.
assumption.
spliter.
apply H7.
apply out_col in H.
apply out_col in H0.
ColR.
Qed.

Lemma plg_uniqueness : A B C D D', Parallelogram A B C D Parallelogram A B C D' D = D'.
intros.
apply plg_mid in H.
apply plg_mid in H0.
ex_and H M.
ex_and H0 M'.
assert(M = M').
eapply l7_17.
apply H.
assumption.
subst M'.
eapply symmetric_point_uniqueness.
apply H1.
assumption.
Qed.

Lemma plgs_trans_trivial : A B C D B', Parallelogram_strict A B C D Parallelogram_strict C D A B'
                                              Parallelogram A B B' A.
intros.
apply plgs_permut in H.
apply plgs_permut in H.
assert (B = B').
eapply plg_uniqueness.
left.
apply H.
left.
assumption.
subst B'.
apply plg_trivial.
apply plgs_diff in H.
spliter.
assumption.
Qed.

Lemma par_strict_trans : A B C D E F, Par_strict A B C D Par_strict C D E F Par A B E F.
intros.
eapply par_trans.
left.
apply H.
left.
assumption.
Qed.

Lemma plgs_pseudo_trans : A B C D E F, Parallelogram_strict A B C D Parallelogram_strict C D E F Parallelogram A B F E.
intros.

induction(eq_dec_points A E).
subst E.
eapply (plgs_trans_trivial A B C D); assumption.

apply plgs_diff in H.
apply plgs_diff in H0.
spliter.

clean_duplicated_hyps.

prolong D C D' D C.

assert(C D').
intro.
subst D'.
apply cong_symmetry in H14.
apply cong_identity in H14.
subst D.
tauto.

assert(HH1:=plgs_par_strict A B C D H).
assert(HH2:=plgs_par_strict C D E F H0).
spliter.

apply par_strict_symmetry in H18.

assert(HH1:= l12_6 C D A B H18).
assert(HH2:= l12_6 C D E F H16).

assert(CongA A D D' B C D').
apply par_preserves_conga_os.
left.
Par.
assumption.
assumption.
apply invert_one_side.
assumption.

assert(CongA E D D' F C D').
apply par_preserves_conga_os.
left.
Par.
assumption.
assumption.
apply invert_one_side.
assumption.

assert(¬ Col A C D).
apply (par_strict_not_col_2 B).
Par.

assert(¬ Col E C D).
apply (par_strict_not_col_2 F).
Par.

assert(HH:=one_or_two_sides C D A E H22 H23).

assert(CongA A D E B C F).

induction HH.

assert(TS C D A F).
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H24.
assumption.

assert(TS C D B F).
eapply l9_8_2.
apply H25.
assumption.

apply(l11_22a A D E D' B C F D').
split.
eapply col_two_sides.
apply bet_col.
apply H2.
intro.
subst D'.
apply between_identity in H2.
subst D.
tauto.
apply invert_two_sides.
assumption.
split.
eapply (col_two_sides _ D).
apply bet_col in H2.
Col.
assumption.
assumption.
split.
assumption.
apply conga_comm.
assumption.

apply(l11_22b A D E D' B C F D').
split.
eapply col_one_side.
apply bet_col.
apply H2.
intro.
subst D'.
apply between_identity in H2.
subst D.
tauto.
apply invert_one_side.
assumption.
split.
eapply (col_one_side _ D).
apply bet_col in H2.
Col.
assumption.
eapply one_side_transitivity.
apply one_side_symmetry.
apply HH1.
apply one_side_symmetry.
eapply one_side_transitivity.
apply one_side_symmetry.
apply HH2.
apply one_side_symmetry.
assumption.
split.
assumption.
apply conga_comm.
assumption.

assert(HP0:=plgs_cong A B C D H).
assert(HP1:=plgs_cong C D E F H0).
spliter.
apply cong_symmetry in H26.

assert(HP:=cong2_conga_cong A D E B C F H24 H28 H26).

assert(Par A B E F).
eapply par_trans.
apply par_symmetry.
left.
apply H18.
left.
assumption.

induction(Col_dec A E F).
induction H29.
apply False_ind.
apply H29.
A.
split; Col.
spliter.

right.
unfold Parallelogram_flat.
repeat split; eCong.
ColR.
ColR.

induction(eq_dec_points A F).
right.
subst F.
intro.
subst E.

apply cong_symmetry in H26.

assert(HQ:=par_strict_cong_mid C A D B H17 H26).
ex_and HQ M.
induction H34.
unfold Midpoint in ×.
spliter.

apply H16.
M.
split; Col.
unfold Midpoint in ×.
spliter.
apply H19.
M.
split.
ColR.
ColR.
left.
assumption.

assert(Par A E B F ¬ Par_strict D C A B ¬ Par_strict D C E F).

eapply(cong3_par2_par ); auto.
repeat split; Cong.
apply par_comm.
left.
assumption.
apply par_symmetry.
left.
assumption.

induction H31.
apply plg_to_parallelogram.
apply pars_par_plg.

assert(Par A B F E).
eapply par_trans.
apply par_symmetry.
left.
apply H18.
apply par_right_comm.
left.
assumption.
induction H32.
assumption.
spliter.
apply False_ind.
apply H30.
Col.
assumption.
induction H31.
apply False_ind.
apply H31.
apply par_strict_left_comm.
assumption.
apply False_ind.
apply H31.
apply par_strict_left_comm.
assumption.
Qed.

Lemma plgf_plgs_trans : A B C D E F, A B Parallelogram_flat A B C D Parallelogram_strict C D E F Parallelogram_strict A B F E.
intros.

induction(eq_dec_points A D).
subst D.
induction H0.
spliter.
apply cong_symmetry in H4.
apply cong_identity in H4.
spliter.
subst C.
apply plgs_comm2.
assumption.

induction(eq_dec_points B C).
subst C.
induction H0.
spliter.
apply cong_identity in H5.
spliter.
subst D.
apply plgs_comm2.
assumption.

assert(HH:=plgs_par_strict C D E F H1).
spliter.

assert(HH:=plgs_cong C D E F H1).
spliter.

assert(HH2:= l12_6 C D E F H4).

assert(HOS := HH2).
induction HH2.
spliter.

unfold TS in H9.
assert(¬ Col F C D).
spliter.
assumption.
spliter.
unfold TS in H8.
assert(¬ Col E C D).
spliter.
assumption.
spliter.

assert(D E).
intro.
subst E.
apply H13.
Col.
assert(HH0:=H0).

induction HH0.
spliter.

prolong D C D' D C.

assert(D D').
intro.
subst D'.
apply between_identity in H22.
subst D.
Col.

assert(C D').
intro.
subst D'.
apply cong_symmetry in H23.
apply cong_identity in H23.
contradiction.

assert(CongA E D D' F C D').

apply(par_preserves_conga_os D E F C D').
apply par_symmetry.
apply par_left_comm.
left.
assumption.
assumption.
intro.
subst D'.
apply cong_symmetry in H23.
apply cong_identity in H23.
subst D.
tauto.
apply invert_one_side.
assumption.

induction(eq_dec_points A C).
subst C.
assert(B=D Midpoint A B D).
eapply l7_20.
Col.
Cong.
induction H27.
induction H21.
tauto.
contradiction.

unfold Parallelogram_strict.
spliter.
split.

apply l9_2.

eapply (l9_8_2 _ _ D).
unfold TS.
repeat split.
intro.
apply H10.
Col.
intro.
apply H10.
ColR.

A.
split.
Col.
apply midpoint_bet.
apply l7_2.
assumption.
eapply l12_6.
assumption.
split.
eapply (par_col_par_2 _ D).
auto.
unfold Midpoint in H27.
spliter.
apply bet_col in H27.
Col.
apply par_right_comm.
left.
assumption.
eCong.

induction(eq_dec_points B D).
subst D.

assert(A=C Midpoint B A C).
eapply l7_20.
Col.
Cong.

induction H28.
tauto.

apply plgs_comm2.
unfold Parallelogram_strict.
split.
apply l9_2.

eapply (l9_8_2 _ _ C).
unfold TS.
repeat split.
auto.
intro.
apply H13.
Col.
intro.
apply H13.
ColR.
B.
split.
Col.
apply midpoint_bet.
apply l7_2.
assumption.