Library GeoCoq.Tarski_dev.Annexes.quadrilaterals


Require Export GeoCoq.Tarski_dev.Ch12_parallel.

Section Quadrilateral.

Context `{T2D:Tarski_2D}.

Lemma cong_identity_inv :
  A B C, A B ¬ Cong A B C C.
Proof.
intros.
intro.
apply H.
eapply cong_identity.
apply H0.
Qed.

Lemma midpoint_midpoint_col : A B A' B' M,
 A B
 Midpoint M A A' Midpoint M B B'
 Col A B B'
 A' B' Col A A' B' Col B A' B'.
Proof.
intros.
assert(A' B').
intro.
apply H.
assert(Cong A' B' A B).
eapply l7_13.
apply H0.
assumption.
apply cong_symmetry in H4.
subst B'.
apply cong_identity in H4.
assumption.

assert(HH0:= H0).
assert(HH1:= H1).
unfold Midpoint in HH0.
unfold Midpoint in HH1.
spliter.

assert(Col M A A').
apply bet_col in H6.
Col.
assert(Col M B B').
apply bet_col in H4.
Col.

induction(eq_dec_points B B').
subst B'.
apply l7_3 in H1.
subst M.
Col5.

assert(Col A A' B').

assert(Col B M A).
eapply col_transitivity_1.
apply H10.
Col.
Col.

assert(Col A M B').

eapply col_transitivity_1.
apply H.
Col.
Col.

induction(eq_dec_points A M).
subst M.
apply cong_symmetry in H7.
apply cong_identity in H7.
subst A'.
Col.

eapply col_transitivity_1.
apply H13.
Col.
Col.
repeat split;
Col.

induction(eq_dec_points A B').
subst B'.
assert(A'=B).
eapply l7_9.
2: apply H1.
apply l7_2.
assumption.
subst A'.
Col.
ColR.
Qed.

Lemma midpoint_par :
  A B A' B' M,
 A B
 Midpoint M A A'
 Midpoint M B B'
 Par A B A' B'.
Proof.
intros.

assert(A' B').
intro.
apply H.
assert(Cong A' B' A B).
eapply l7_13.
apply H0.
assumption.
apply cong_symmetry in H3.
subst B'.
apply cong_identity in H3.
assumption.

induction(Col_dec A B B').
assert(A' B' Col A A' B' Col B A' B').
eapply (midpoint_midpoint_col _ _ _ _ M); auto.

unfold Par.
right.
split; auto.

assert(HH0:= H0).
assert(HH1:= H1).
unfold Midpoint in HH0.
unfold Midpoint in HH1.
spliter.

assert(Col M A A').
apply bet_col in H6.
Col.
assert(Col M B B').
apply bet_col in H4.
Col.

unfold Par.
left.
unfold Par_strict.
repeat split; auto; try apply all_coplanar.
intro.
ex_and H10 X.

prolong X M X' M X.
assert(Col A' B' X').
eapply mid_preserves_col.
2: apply H0.
2: apply H1.
apply col_permutation_1.
apply H10.
unfold Midpoint.
split.
assumption.
apply cong_left_commutativity.
Cong.

assert(Col B' X X').
eapply (col_transitivity_1 _ A').
auto.
Col.
Col.
induction(eq_dec_points X X').
subst X'.
apply between_identity in H12.
subst X.

apply H3.
induction(eq_dec_points B M).
subst M.
apply cong_symmetry in H5.
apply cong_identity in H5.
subst B'.
Col.
apply col_permutation_2.
apply (col_transitivity_1 _ M); Col.

assert(Col X M B').
apply bet_col in H12.
apply (col_transitivity_1 _ X'); Col.

assert(Col X' M B').
apply bet_col in H12.
apply (col_transitivity_1 _ X); Col.

assert(Col M B X).
eapply (col_transitivity_1 ).
2: apply col_permutation_5.
2: apply H9.
intro.
subst B'.
apply cong_identity in H5.
subst B.

apply H3.
Col.
Col.

assert(Col X M A).
eapply (col_transitivity_1 ).
2: apply col_permutation_3.
2:apply H19.
intro.
subst X.

assert(Cong M X' M B').
eapply cong_transitivity.
apply H13.
Cong.
assert (HH:=l7_20 M X' B' H18 H20).
induction HH.
subst X'.
apply H3.
apply col_permutation_2.
apply (col_transitivity_1 _ M).
intro.
subst M.
apply cong_identity in H13.
contradiction.
Col.

assert(Col M B A').
ColR.
induction(eq_dec_points M A').
subst A'.
apply cong_identity in H7.
subst A.
Col.
ColR.
assert(X'= B).
eapply l7_9.
apply H21.
assumption.
subst X'.
tauto.
Col.
apply H3.
eapply col3.
2: apply H20.
intro.
subst X.
apply cong_identity in H13.
subst X'.
tauto.
Col.
Col.
Qed.

Lemma midpoint_par_strict :
  A B A' B' M,
 A B
 ¬ Col A B B'
 Midpoint M A A'
 Midpoint M B B'
 Par_strict A B A' B'.
Proof.
intros.
assert(Par A B A' B').
eapply (midpoint_par A B A' B' M); assumption.
induction H3.
assumption.
spliter.
apply False_ind.

assert(HH:=midpoint_midpoint_col B' A' B A M).
assert(B A Col B' B A Col A' B A).
apply HH.
auto.
apply l7_2.
assumption.
apply l7_2.
assumption.
Col.
spliter.
apply H0.
Col.
Qed.

Lemma le_left_comm : A B C D, Le A B C D Le B A C D.
intros.
unfold Le in ×.
ex_and H P.
P.
split.
assumption.
Cong.
Qed.

Lemma le_right_comm : A B C D, Le A B C D Le A B D C.
intros.
induction(eq_dec_points D C).
subst D.
apply le_zero in H.
subst B.
eapply le_trivial.

induction(eq_dec_points A B).
subst B.
apply le_trivial.

assert(HH:=segment_construction_3 D C A B H0 H1).
ex_and HH P'.
unfold Out in H2.
spliter.
induction H5.

assert(Le D C A B).
eapply l5_5_2.
P'.
split; auto.
apply le_left_comm in H6.
assert(Cong A B C D).
apply le_anti_symmetry.
auto.
auto.
unfold Le.
C.
split.
apply between_trivial.
Cong.
unfold Le.
P'.
split.
assumption.
Cong.
Qed.

Lemma le_comm :
  A B C D, Le A B C D Le B A D C.
Proof.
intros.
apply le_left_comm.
apply le_right_comm.
assumption.
Qed.

Lemma le_cong_le :
  A B C A' B' C',
 Bet A B C
 Bet A' B' C'
 Le A B A' B'
 Cong B C B' C'
 Le A C A' C'.
Proof.
intros.
eapply l5_5_2.
unfold Le in H1.
ex_and H1 P.
prolong A C T P B'.
T.
split.
assumption.

assert(Bet A B T).
eapply between_exchange4.
apply H.
assumption.

eapply l2_11.
apply H6.
2: apply H3.
eapply between_exchange4.
apply H1.
assumption.
apply cong_left_commutativity.
eapply l2_11.
4: apply cong_left_commutativity.
4:apply H2.
apply between_symmetry.
eapply between_exchange3.
apply H.
assumption.
eapply between_exchange3.
apply H1.
assumption.
Cong.
Qed.

Lemma cong_le_le :
  A B C A' B' C',
 Bet A B C
 Bet A' B' C'
 Le B C B' C'
 Cong A B A' B'
 Le A C A' C'.
Proof.
intros.
apply le_comm.
eapply le_cong_le.
apply between_symmetry.
apply H.
apply between_symmetry.
apply H0.
apply le_comm.
assumption.
Cong.
Qed.

Lemma bet3_cong3_bet : A B C D D', A B A C A D Bet D A C Bet A C B Bet D C D' Cong A B C D Cong A D B C Cong D C C D'
                               Bet C B D'.
intros.
assert(Bet D C B).
eBetween.
assert(B C).
intro.
subst C.
apply cong_identity in H6.
contradiction.

assert(D' C).
intro.
subst D'.
apply cong_identity in H7.
subst D.
apply cong_identity in H5.
contradiction.

assert(D C).
intro.
subst D.
apply cong_identity in H5.
contradiction.

assert (Out C B D').
repeat split; auto.
eapply (l5_2 D); auto.

assert(Out D B D').
repeat split; auto.

intro.
subst D.
apply between_identity in H8.
contradiction.
intro.
subst D'.
apply between_identity in H4.
contradiction.

eapply (l5_1 _ C); auto.

assert(Le D A D C).
unfold Le.
A.
split; Cong.

assert(Le D B D D').
eapply (le_cong_le _ A _ _ C).
eBetween.
assumption.
assumption.
eCong.

assert(Bet D B D').

apply l6_13_1; auto.
eapply (between_exchange3 D); auto.
Qed.

Lemma bet_le_le :
  A B C A' B' C',
 Bet A B C
 Bet A' B' C'
 Le A B A' B'
 Le B C B' C'
 Le A C A' C'.
Proof.
intros.
assert(HH1:=H1).
assert(HH2:=H2).
unfold Le in HH1.
unfold Le in HH2.
ex_and HH1 X.
ex_and HH2 Y.
assert(Le A C A' Y).
eapply le_cong_le.
3: apply H1.
apply H.
eBetween.
assumption.

induction (eq_dec_points B' Y).
subst Y.

assert(Le A' B' A' C').
unfold Le.
B'.
split.
assumption.
apply cong_reflexivity.
eapply le_transitivity.
apply H7.
assumption.

assert(Bet A' Y C').
eapply outer_transitivity_between2.
2: apply H5.

eapply between_inner_transitivity.
apply H0.
assumption.
assumption.
eapply le_transitivity.
apply H7.
unfold Le.
Y.
split.
assumption.
apply cong_reflexivity.
Qed.

Lemma bet_double_bet :
  A B C B' C',
 Midpoint B' A B
 Midpoint C' A C
 Bet A B' C'
 Bet A B C.
Proof.
intros.
unfold Midpoint in ×.
spliter.
assert(Le A B' A C').
unfold Le.
B'.
split.
assumption.
apply cong_reflexivity.
assert (Le B' B C' C).
eapply l5_6.
apply H4.
auto.
auto.
assert(Le A B A C).
eapply bet_le_le.
apply H.
apply H0.
assumption.
assumption.

induction (eq_dec_points A B').
subst B'.
apply cong_symmetry in H3.
apply cong_identity in H3.
subst B.
apply between_trivial2.

assert( A C').
intro.
subst C'.
apply le_zero in H4.
contradiction.

assert(A B).
intro.
subst B.
apply between_identity in H.
contradiction.
assert(A C).
intro.
subst C.
apply between_identity in H0.
contradiction.

assert(Out A B C).

assert(Bet A B C' Bet A C' B).
eapply l5_1.
apply H7.
assumption.
assumption.
induction H11.

eapply l6_7.
apply bet_out.
auto.
2: apply H11.
auto.
apply bet_out.
auto.
auto.
assumption.

assert(Bet A B C Bet A C B).
eapply l5_1.
2: apply H11.
assumption.
assumption.
induction H12.
apply bet_out.
auto.
auto.
assumption.
apply l6_6.
apply bet_out.
auto.
auto.
assumption.
eapply l6_13_1.
assumption.
assumption.
Qed.

Lemma bet_half_bet :
  A B C B' C',
 Bet A B C
 Midpoint B' A B
 Midpoint C' A C
 Bet A B' C'.
Proof.
intros.
assert(HH0:= H0).
assert(HH1:= H1).
unfold Midpoint in H0.
unfold Midpoint in H1.
spliter.

induction(eq_dec_points A B).
subst B.
apply between_identity in H0.
subst B'.
apply between_trivial2.
assert(A C).
intro.
subst C.
apply between_identity in H1.
subst C'.
apply between_identity in H.
contradiction.
assert(A B').
intro.
subst B'.
apply cong_symmetry in H3.
apply cong_identity in H3.
contradiction.
assert(A C').
intro.
subst C'.
apply cong_symmetry in H2.
apply cong_identity in H2.
contradiction.

assert(Col A B' C').
apply bet_col in H0.
apply bet_col in H1.
apply bet_col in H.
ColR.
induction H8.
assumption.
induction H8.
apply between_symmetry in H8.

assert(Bet A C B).
eapply bet_double_bet.
apply HH1.
apply HH0.
assumption.

assert(B = C).
eapply between_equality.
apply between_symmetry.
apply H9.
Between.
subst C.
assert(B' = C').
eapply l7_17.
apply HH0.
assumption.
subst C'.
apply between_trivial.


assert(Bet A B' C).
eapply between_exchange4.
apply H0.
assumption.

assert(Out A B' C').
unfold Out.
repeat split; auto.
eapply l5_3.
apply H9.
assumption.
eapply l6_4_1 in H10.
spliter.
apply between_symmetry in H8.
contradiction.
Qed.

Lemma midpoint_preserves_bet :
  A B C B' C',
  Midpoint B' A B
  Midpoint C' A C
 (Bet A B C Bet A B' C').
Proof.
intros.
split.
intro.
eapply bet_half_bet.
apply H1.
assumption.
assumption.
intro.
eapply bet_double_bet.
apply H.
apply H0.
assumption.
Qed.

Lemma symmetry_preseves_bet1 :
  A B M A' B',
  Midpoint M A A'
  Midpoint M B B'
  Bet M A B
  Bet M A' B'.
Proof.
intros.
eapply l7_15.
2: apply H.
2: apply H0.
2: apply H1.
apply l7_3_2.
Qed.

Lemma symmetry_preseves_bet2 :
  A B M A' B',
  Midpoint M A A'
  Midpoint M B B'
  Bet M A' B'
  Bet M A B.
Proof.
intros.
eapply l7_15.
apply l7_3_2.
apply l7_2.
apply H.
apply l7_2.
apply H0.
assumption.
Qed.

Lemma symmetry_preserves_bet :
  A B M A' B',
  Midpoint M A A'
  Midpoint M B B'
 (Bet M A' B' Bet M A B).
Proof.
intros.
split.
apply symmetry_preseves_bet2;
assumption.
intro.
eapply (symmetry_preseves_bet1 A B);
assumption.
Qed.

Lemma bet_cong_bet :
  A B C D,
  A B
  Bet A B C
  Bet A B D
  Cong A D B C
  Bet B D C.
Proof.
intros.

assert(Bet B C D Bet B D C).
eapply (l5_2 A); assumption.
induction H3.

assert(Le B C B D).
eapply l5_5_2.
D.
split.
assumption.
Cong.

assert(Le D B D A).
eapply l5_5_2.

A.
split.
Between.
Cong.

assert(Cong B C B D).
eapply le_anti_symmetry.
assumption.
eapply l5_6.
apply H5.
Cong.
Cong.

assert(C=D).
eapply between_cong.
apply H3.
assumption.
subst D.
assert(B = A).
eapply (between_cong C).
Between.
Cong.
subst A.
tauto.
assumption.
Qed.

Lemma col_cong_mid :
  A B A' B',
  Par 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.
unfold Par in H.
induction H.
contradiction.
spliter.

induction (eq_dec_points A A').
subst A'.
assert(B = B' Midpoint A B B').
eapply l7_20; auto.
induction H5.
subst B'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
M.
right.
split.
assumption.
apply l7_2.
assumption.
A.
left.
split.
apply l7_3_2.
assumption.

induction (eq_dec_points B B').
subst B'.
assert(A = A' Midpoint B A A').
eapply l7_20.
Col.
Cong.
induction H6.
subst A'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
M.
right.
split.
assumption.
apply l7_2.
assumption.
B.
left.
split.
assumption.
apply l7_3_2.

induction (eq_dec_points A B').
subst B'.
assert(B = A' Midpoint A B A').
eapply l7_20.
Col.
Cong.
induction H7.
subst A'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
M.
left.
split.
assumption.
apply l7_2.
assumption.
A.
right.
split.
apply l7_3_2.
assumption.

induction (eq_dec_points A' B).
subst A'.
assert(A = B' Midpoint B A B').
eapply l7_20.
Col.
Cong.
induction H8.
subst B'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
M.
left.
split.
assumption.
apply l7_2.
assumption.
B.
right.
split.
assumption.
apply l7_3_2.

assert(Col A B A').
ColR.
assert(Col A B B').
ColR.

induction H10.
induction H4.

assert( HH:= midpoint_existence A' B).
ex_and HH M.
M.
right.
assert(HH:= H11).
unfold Midpoint in HH.
spliter.
split.

assert(Bet B M B').

eapply between_exchange4.
2: apply H4.
Between.

assert(Bet A M B').
eapply between_exchange2.
apply H10.
assumption.
assert(Cong A M B' M).
eapply (l2_11 A B _ _ A').
eapply between_inner_transitivity.
apply H10.
assumption.
eapply between_inner_transitivity.
apply between_symmetry.
apply H4.

assumption.
Cong.
Cong.

unfold Midpoint.
split.
assumption.
Cong.
apply l7_2.
assumption.

induction H4.

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

assert(HH:= H11).
unfold Midpoint in HH.
spliter.

split.

assert(Bet A' M B).
eapply between_exchange2.
apply H4.
Between.
assert(Bet M B A).
eapply between_exchange3.

apply between_symmetry.
apply H12.
Between.

assert(Bet A' M A).
eapply outer_transitivity_between.
apply H14.
assumption.
intro.
subst M.
apply is_midpoint_id in H11.
contradiction.
assert(Cong A M A' M).
eapply l2_11.
apply between_symmetry.
apply H15.
eapply between_inner_transitivity.
apply H4.
Between.
assumption.
Cong.
unfold Midpoint.
split.
Between.
Cong.
assumption.

assert(Bet B A' A).
eapply (bet_cong_bet B').
auto.
Between.
Between.
Cong.

assert( HH:= midpoint_existence A' B).
ex_and HH M.
M.
right.
assert(HH:=H12).
unfold Midpoint in HH.
spliter.

split.
assert(Bet B M A).
eapply between_exchange4.
apply between_symmetry.
apply H13.
assumption.

assert(Bet B' B M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H10.
assumption.

assert(Bet M A' A).
eapply between_exchange3.
2:apply H11.
Between.
assert(Bet B' M A').
eapply outer_transitivity_between2.
apply H16.
Between.
intro.
subst M.
apply l7_2 in H12.
apply is_midpoint_id in H12.
auto.
assert(Bet B' M A).
eapply outer_transitivity_between.
apply H18.
assumption.
intro.
subst A'.
apply is_midpoint_id in H12.
subst M.
tauto.

assert(Cong A M B' M).
eapply l4_3.
apply between_symmetry.
apply H15.
apply H18.
Cong.
Cong.
unfold Midpoint.
split.
Between.
Cong.
Midpoint.

induction H10.
induction H3.

assert(B' = B A = A').
eapply bet_cong_eq.
assumption.
Between.
Cong.
spliter.
contradiction.
induction H3.

assert(Bet B' B A').
eapply bet_cong_bet.
apply H7.
Between.
Between.
Cong.

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

assert(HH:=H12).
unfold Midpoint in HH.
spliter.
left.

split.

assert(Bet A' M B').
eapply between_exchange2.
apply between_symmetry.
apply H11.
assumption.

assert(Bet M B' A).
eapply between_exchange3.
apply H13.
assumption.
assert(Bet A' M A).
eapply outer_transitivity_between.
apply H15.
assumption.
intro.
subst M.
apply l7_2 in H12.
apply is_midpoint_id in H12.
subst B'.
tauto.

assert(Bet A M B).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H16.
Between.
intro.
subst M.
apply l7_2 in H12.
apply is_midpoint_id in H12.
subst B'.
tauto.

assert(Cong A' M A M).
eapply l4_3.
apply H15.
apply H18.
Cong.
Cong.
unfold Midpoint.
split.
Between.
Cong.
assumption.

assert( HH:= midpoint_existence A B').
ex_and HH M.
M.
assert(HH:=H11).
unfold Midpoint in HH.
spliter.
right.
split.
assumption.

assert(Bet A' A M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H3.
assumption.

assert(Bet A M B).
eapply between_exchange4.
apply H11.
Between.

assert(Bet A' M B).
eapply outer_transitivity_between2.
apply H14.
assumption.
intro.
subst M.
apply is_midpoint_id in H11.
contradiction.

assert(Cong B M A' M).
eapply l4_3.
apply between_symmetry.
apply H15.
eapply between_exchange2.
apply between_symmetry.
apply H3.
assumption.
Cong.
Cong.
unfold Midpoint.
split.
Between.
Cong.

induction H9.

assert(Bet B' B A').
eapply outer_transitivity_between2.
apply H10.
assumption.
assumption.

assert(B = A' B' = A).
eapply bet_cong_eq.
assumption.
assumption.
Cong.
spliter.
subst A'.
tauto.

induction H9.

assert( HH:= midpoint_existence A A').
ex_and HH M.
M.
assert(HH:=H11).
unfold Midpoint in HH.
spliter.
left.
split.
assumption.

assert(Bet B A' M).
eapply between_inner_transitivity.
apply H9.
Between.

assert(Bet B M A).
eapply outer_transitivity_between2.
apply H14.
Between.
intro.
subst M.
apply l7_2 in H11.
apply is_midpoint_id in H11.
subst A'.
tauto.

assert(Bet B M B').
eapply between_exchange4.
apply H15.
Between.

assert(Cong B M B' M).
eapply l4_3.
apply H15.

assert(Bet B' A A').
eapply between_inner_transitivity.
apply H10.
Between.
eapply between_exchange2.
apply H17.
assumption.
Cong.
Cong.
unfold Midpoint.
split.
assumption.
Cong.

assert(Bet A B' A' Bet A A' B').
eapply (l5_2 B).
auto.
Between.
Between.
induction H11.

assert( HH:= midpoint_existence A B').
ex_and HH M.
M.
assert(HH:=H12).
unfold Midpoint in HH.
spliter.
right.
split.
assumption.

assert(Bet B M B').
eapply between_exchange2.
apply between_symmetry.
apply H10.
assumption.
assert(Bet A' B' M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H11.
Between.

assert(Bet A' M B).
eapply outer_transitivity_between2.
apply H16.
Between.
intro.
subst M.
apply l7_2 in H12.
apply is_midpoint_id in H12.
subst B'.
tauto.

assert(Cong M A' M B).
eapply l2_11.
apply between_symmetry.
apply H16.
eapply between_exchange3.
apply between_symmetry.
apply H13.
assumption.
Cong.
Cong.
unfold Midpoint.
split.
Between.
Cong.

assert( HH:= midpoint_existence A A').
ex_and HH M.
M.
assert(HH:=H12).
unfold Midpoint in HH.
spliter.
left.
split.
assumption.

assert(Bet B A M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H9.
assumption.
assert(Bet B' M A).
eapply between_exchange2.
apply between_symmetry.
apply H11.
Between.
assert(Bet B' M B).
eapply outer_transitivity_between.
apply H16.
Between.
intro.
subst M.
apply is_midpoint_id in H12.
contradiction.
assert(Cong B' M B M).
eapply l2_11.
eapply between_inner_transitivity.
apply between_symmetry.
apply H11.
Between.
apply H15.
Cong.
Cong.
unfold Midpoint.
split.
Between.
Cong.
Qed.

Lemma mid_par_cong1 :
  A B A' B' M,
  A B
  Midpoint M A A'
  Midpoint M B B'
  Cong A B A' B' Par A B A' B'.
Proof.
intros.
split.
eapply (l7_13 M);
Midpoint.
apply (midpoint_par _ _ _ _ M); auto.
Qed.

Lemma mid_par_cong2 :
  A B A' B' M,
  A B'
  Midpoint M A A'
  Midpoint M B B'
  Cong A B' A' B Par A B' A' B.
Proof.
intros.
spliter.
split.
apply (l7_13 M); Midpoint.
eapply (midpoint_par _ _ _ _ M); Midpoint.
Qed.

Lemma mid_par_cong :
  A B A' B' M,
  A B A B'
  Midpoint M A A'
  Midpoint M B B'
  Cong A B A' B' Cong A B' A' B Par A B A' B' Par A B' A' B.
Proof.
intros.
spliter.
assert(Cong A B A' B' Par A B A' B').
eapply (mid_par_cong1 _ _ _ _ M); Midpoint.
assert(Cong A B' A' B Par A B' A' B).
apply (mid_par_cong2 _ _ _ _ M);Midpoint.
spliter.
repeat split;
assumption.
Qed.

Parallelogram

Definition Parallelogram_strict A B A' B' := TS A A' B B' Par A B A' B' Cong A B A' B'.

Definition Parallelogram_flat A B A' B' :=
  Col A B A' Col A B B'
  Cong A B A' B' Cong A B' A' B
  (A A' B B').

Definition Parallelogram A B A' B' := Parallelogram_strict A B A' B' Parallelogram_flat A B A' B'.

Lemma Parallelogram_strict_Parallelogram :
  A B C D,
  Parallelogram_strict A B C D Parallelogram A B C D.
Proof.
unfold Parallelogram.
tauto.
Qed.

Lemma plgf_permut :
  A B C D,
  Parallelogram_flat A B C D
  Parallelogram_flat B C D A.
Proof.
intros.
unfold Parallelogram_flat in ×.
spliter.
induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
repeat split; Col.
apply cong_trivial_identity.
induction H3;
left; assumption.

assert(C D).
intro.
subst D.
apply cong_identity in H1.
contradiction.
repeat split.
ColR.
Col.
Cong.
Cong.
induction H3.
right.
auto.
left; assumption.
Qed.

Lemma plgf_sym :
  A B C D,
 Parallelogram_flat A B C D
 Parallelogram_flat C D A B.
Proof.
intros.
apply plgf_permut.
apply plgf_permut.
assumption.
Qed.

Lemma plgf_irreflexive :
  A B,
 ¬ Parallelogram_flat A B A B.
Proof.
intros.
unfold Parallelogram_flat.
intro.
spliter.
induction H3; tauto.
Qed.

Lemma plgs_irreflexive :
  A B,
  ¬ Parallelogram_strict A B A B.
Proof.
intros.
intro.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.
apply H2.
Col.
Qed.

Lemma plg_irreflexive :
  A B,
 ¬ Parallelogram A B A B.
Proof.
intros.
intro.
induction H.
apply plgs_irreflexive in H.
assumption.
apply plgf_irreflexive in H.
assumption.
Qed.

Lemma plgf_mid :
  A B C D,
  Parallelogram_flat A B C D
   M, Midpoint M A C Midpoint M B D.
Proof.
intros.
unfold Parallelogram_flat in H.
spliter.

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
assert(HH:=midpoint_existence A C).
ex_and HH M.
M.
split; assumption.
assert(C D).
intro.
subst D.
apply cong_identity in H1.
contradiction.

assert(Par A B C D).
apply par_symmetry.
unfold Par.
right.
repeat split; Col.

assert(¬Par_strict A B C D).
intro.
unfold Par_strict in H7.
spliter.
apply H10.
C.
split; Col.

assert(HH:= col_cong_mid A B C D H6 H7 H1).
ex_and HH M.
induction H8.
M.
assumption.
spliter.
induction(eq_dec_points B C).
subst C.
apply cong_identity in H2.
subst D.
apply l7_3 in H8.
apply l7_3 in H9.
subst M.
contradiction.
assert(A D).
intro.
subst D.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst C.
tauto.

apply False_ind.
assert(Col A B M).
unfold Midpoint in ×.
spliter.
eapply (col_transitivity_1 _ D).
assumption.
Col.
apply bet_col in H8.
Col.

assert(B M).
intro.
subst M.
apply is_midpoint_id in H9.
contradiction.

assert(A M).
intro.
subst M.
apply is_midpoint_id in H8.
contradiction.

induction H12.

assert(HH:=symmetry_preserves_bet B A M C D H9 H8).
destruct HH.
assert(Bet M C D).
apply H16.
Between.
clear H15 H16.

assert(B = A D = C).
unfold Midpoint in ×.
spliter.
apply bet_cong_eq.

eBetween.
eBetween.
Cong.
spliter.
subst B.
tauto.

induction H12.

assert(Bet M A C Bet M C A).
unfold Midpoint in ×.
spliter.
eapply (l5_2 B); assumption.
induction H15.

assert(Bet M D B Bet M A C).
apply(symmetry_preserves_bet A C M D B).
assumption.
Midpoint.
destruct H16.
assert(Bet M D B).
apply H17.
assumption.
clear H17 H16.

assert(A = C B = D).
unfold Midpoint in ×.
spliter.
apply bet_cong_eq.
eBetween.
eBetween.
Cong.
spliter.
subst C.
induction H3.
tauto.
subst D.
tauto.

assert(Bet M B D Bet M C A).
apply(symmetry_preserves_bet); Midpoint.
destruct H16.
assert(Bet M B D).
apply H17.
assumption.
clear H16 H17.

assert(C = A D = B).
unfold Midpoint in ×.
spliter.
apply bet_cong_eq.
eBetween.
eBetween.
Cong.
spliter.
subst C.
induction H3.
tauto.
subst D.
tauto.

assert(HH:=symmetry_preserves_bet A B M D C H8 H9).
destruct HH.
assert(Bet M D C).
apply H16.
Between.
clear H15 H16.

assert(A = B C = D).
unfold Midpoint in ×.
spliter.
apply bet_cong_eq.

eBetween.
eBetween.
Cong.
spliter.
subst B.
tauto.
Qed.

Lemma mid_plgs :
  A B C D M,
  ¬ Col A B C
  Midpoint M A C Midpoint M B D
  Parallelogram_strict A B C D.
Proof.
intros.
unfold Parallelogram_strict.
assert(A C).
intro.
apply H.
subst C.
Col.

assert(B D).
intro.
subst D.
apply l7_3 in H1.
subst M.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
contradiction.

assert(M D).
intro.
subst M.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst D.
tauto.

assert( M A).
intro.
subst M.
apply is_midpoint_id in H0.
contradiction.
repeat split.

intro.
apply H.
Col.
intro.
unfold Midpoint in ×.
spliter.
apply bet_col in H0.
apply bet_col in H1.
apply H.
assert(Col M A D).
ColR.
assert(Col M A B).
ColR.
ColR.
M.
unfold Midpoint in ×.
spliter.
split.
apply bet_col in H0.
Col.
apply H1.
apply (midpoint_par _ _ _ _ M).
intro.
subst B.
apply H.
Col.
assumption.
assumption.
eapply (l7_13 M); Midpoint.
Qed.

Lemma mid_plgf_aux :
  A B C D M,
  A C
  Col A B C
  Midpoint M A C Midpoint M B D
  Parallelogram_flat A B C D.
Proof.
intros.
unfold Parallelogram_flat.
induction(eq_dec_points B D).
subst D.
apply l7_3 in H2.
subst M.
unfold Midpoint in H1.
spliter.
repeat split; Col.
Cong.
Cong.

assert(Col A B M).
unfold Midpoint in ×.
spliter.
apply bet_col in H1.
apply bet_col in H2.
ColR.
assert(M B).
intro.
subst M.
apply is_midpoint_id in H2.
contradiction.

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

induction H4.

assert(HH:=symmetry_preserves_bet B A M D C H2 H1).
destruct HH.
assert(Bet M D C).
apply H8.
Between.
clear H8 H7.

repeat split.
Col.
unfold Midpoint in ×.
spliter.
apply bet_col in H2.
apply bet_col in H1.
apply bet_col in H4.
ColR.

eapply l4_3.
apply H4.
apply between_symmetry.
apply H9.
unfold Midpoint in H1.
spliter.
Cong.
unfold Midpoint in H2.
spliter.
Cong.

unfold Midpoint in ×.
spliter.
eapply (l2_11 _ M _ _ M _).
eBetween.
eBetween.
Cong.
Cong.
left.
assumption.

induction H4.

assert(Bet M A D Bet M D A).
eapply (l5_2 B).
auto.
assumption.
unfold Midpoint in H2.
spliter.
assumption.
induction H7.

assert(Bet M C B Bet M A D).

apply (symmetry_preserves_bet A D M C B).
assumption.
Midpoint.
destruct H8.
assert(Bet M C B).
apply H9.
assumption.
clear H9 H8.

unfold Midpoint in ×.
spliter.
repeat split.
assumption.
apply bet_col in H4.
apply bet_col in H1.
apply bet_col in H2.
ColR.
eapply (l2_11 _ M _ _ M _).
Between.
eBetween.
Cong.
Cong.
apply cong_commutativity.
eapply (l4_3).
apply between_symmetry.
apply H7.
apply between_symmetry.
apply H10.
Cong.
Cong.
left.
assumption.

assert(Bet M B C Bet M D A).

apply (symmetry_preserves_bet D A M B C).
Midpoint.
Midpoint.
destruct H8.
assert(Bet M B C).
apply H9.
assumption.
clear H8 H9.
unfold Midpoint in ×.
spliter.
repeat split.
assumption.
apply bet_col in H4.
apply bet_col in H1.
apply bet_col in H2.
ColR.

eapply (l2_11 _ M _ _ M _).
Between.
eBetween.
Cong.
Cong.

eapply l4_3.
apply between_symmetry.
apply H7.
apply between_symmetry.
apply H10.
Cong.
Cong.
left.
assumption.

assert(Bet M C D Bet M A B).
apply (symmetry_preserves_bet A B M C D H1 H2).

destruct H7.
assert(Bet M C D).
apply H8.
assumption.
clear H8 H7.

repeat split.
Col.
unfold Midpoint in ×.
spliter.
apply bet_col in H2.
apply bet_col in H1.
apply bet_col in H4.
ColR.
apply cong_commutativity.
eapply l4_3.
apply between_symmetry.
apply H4.
apply between_symmetry.
apply H9.
unfold Midpoint in H2.
spliter.
Cong.
unfold Midpoint in H1.
spliter.
Cong.

unfold Midpoint in ×.
spliter.
eapply (l2_11 _ M _ _ M _).
eBetween.
eBetween.
Cong.
Cong.
left.
assumption.
Qed.

Lemma mid_plgf :
  A B C D M,
  (A C B D )
  Col A B C
  Midpoint M A C Midpoint M B D
  Parallelogram_flat A B C D.
Proof.
intros.
induction H.
eapply (mid_plgf_aux A B C D M); assumption.
apply plgf_sym.
induction(eq_dec_points A C).
subst C.
spliter.
apply l7_3 in H1.
subst M.
unfold Midpoint in H2.
spliter.
unfold Parallelogram_flat.
repeat split.
Col.
apply bet_col in H1.
Col.
Cong.
Cong.
right.
auto.
spliter.
eapply (mid_plgf_aux C D A B M).
auto.
unfold Midpoint in ×.
spliter.
apply bet_col in H1.
apply bet_col in H2.

assert( M C).
intro.
subst M.
apply cong_identity in H5.
contradiction.

assert( M B).
intro.
subst M.
apply cong_symmetry in H4.
apply cong_identity in H4.
contradiction.
ColR.
Midpoint.
Midpoint.
Qed.

Lemma mid_plg :
  A B C D M,
 (A C B D )
 Midpoint M A C Midpoint M B D
 Parallelogram A B C D.
Proof.
intros.
unfold Parallelogram.

induction(Col_dec A B C).
right.
apply (mid_plgf _ _ _ _ M);
assumption.
left.
apply (mid_plgs _ _ _ _ M);
assumption.
Qed.

Lemma mid_plg_1 :
  A B C D M,
 A C
 Midpoint M A C Midpoint M B D
 Parallelogram A B C D.
Proof.
intros.
apply mid_plg with M; intuition.
Qed.

Lemma mid_plg_2 :
  A B C D M,
 B D
 Midpoint M A C Midpoint M B D
 Parallelogram A B C D.
Proof.
intros.
apply mid_plg with M; intuition.
Qed.

Lemma midpoint_cong_uniqueness :
  A B C D M,
  Col A B C
  Midpoint M A B Midpoint M C D
  Cong A B C D
  A = C B = D A = D B = C.
Proof.
intros.

induction (eq_dec_points A B).
subst B.
spliter.
apply l7_3 in H0.
subst M.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
apply l7_3 in H2.
left.
split; assumption.

induction(eq_dec_points A C).
left.
split.
assumption.
subst C.
spliter.
eapply symmetric_point_uniqueness.
apply H0.
assumption.
right.
spliter.
assert(HH:=cong_cong_half_1 A M B C M D H0 H4 H1).
assert(A = C Midpoint M A C).
apply l7_20.
unfold Midpoint in ×.
spliter.
apply bet_col in H0.
apply bet_col in H4.
ColR.
Cong.
induction H5.
contradiction.
assert(B = C).
eapply symmetric_point_uniqueness.
apply H0.
assumption.
split.
subst C.
eapply symmetric_point_uniqueness.
apply l7_2.
apply H0.
assumption.
assumption.
Qed.

Lemma plgf_not_comm :
  A B C D, A B
  Parallelogram_flat A B C D
  ¬ Parallelogram_flat A B D C ¬ Parallelogram_flat B A C D.
Proof.
intros.

assert(HH0:=plgf_mid A B C D H0).
split.
intro.
assert(HH1:=plgf_mid A B D C H1).

unfold Parallelogram_flat in ×.
spliter.
ex_and HH0 M.

assert(A = B C = D A = D C = B).
apply(midpoint_cong_uniqueness A C B D M).
Col.
split; assumption.
Cong.
induction H12.
spliter.
contradiction.
spliter.
subst D.
subst C.
induction H5; tauto.

ex_and HH0 M.
unfold Parallelogram_flat in ×.
intro.
spliter.
assert(A = B C = D A = D C = B).
apply(midpoint_cong_uniqueness A C B D M).
Col.
split; assumption.
Cong.
induction H12.
spliter.
contradiction.
spliter.
subst D.
subst C.
induction H7; tauto.
Qed.

Lemma plgf_cong :
  A B C D,
  Parallelogram_flat A B C D
  Cong A B C D Cong A D B C.
Proof.
intros.
unfold Parallelogram_flat in H.
spliter.
split; Cong.
Qed.

Definition Plg A B C D := (A C B D) M, Midpoint M A C Midpoint M B D.

Lemma plg_to_parallelogram : A B C D, Plg A B C D Parallelogram A B C D.
intros.
unfold Plg in H.
spliter.
ex_and H0 M.
eapply (mid_plg _ _ _ _ M).
induction H;[left|right]; assumption.
assumption.
assumption.
Qed.

Lemma plgs_one_side :
  A B C D,
 Parallelogram_strict A B C D
 OS A B C D OS C D A B.
Proof.
intros.
unfold Parallelogram_strict in H.
spliter.
induction H0.
split.
apply l12_6.
assumption.
apply par_strict_symmetry in H0.
apply l12_6.
assumption.
apply False_ind.
spliter.
unfold TS in H.
spliter.
apply H5.
Col.
Qed.

Lemma parallelogram_strict_not_col : A B C D,
 Parallelogram_strict A B C D
 ¬ Col A B C.
Proof.
unfold Parallelogram_strict.
intros.
spliter.
apply two_sides_not_col in H.
Col.
Qed.

Rhombus

Definition Rhombus A B C D := Plg A B C D Cong A B B C.

Lemma Rhombus_Plg : A B C D, Rhombus A B C D Plg A B C D.
Proof.
unfold Rhombus.
tauto.
Qed.

Lemma ex_col3 : A B C, Col A B C D, Col A B D A D B D C D.
intros.
induction(eq_dec_points A B).
subst B.
assert(HH:=ex_col2 A C).
ex_and HH X.
X.
split; Col.
induction(eq_dec_points B C).
subst C.
assert(HH:=ex_col2 A B).
ex_and HH X.
X.
repeat split; Col.
induction (eq_dec_points A C).
subst C.
assert(HH:=ex_col2 A B).
ex_and HH X.
X.
repeat split; Col.

induction H.
prolong B C X B C.
X.
repeat split; try (intro; subst X).
apply bet_col.
eBetween.
apply H1.
eapply between_equality.
apply H3.
Between.
apply between_identity in H3.
contradiction.
apply cong_symmetry in H4.
apply cong_identity in H4.
contradiction.

induction H.
prolong C A X C A.
X.
repeat split; try (intro; subst X).
assert(Bet B A X).
eBetween.
apply bet_col in H5.
Col.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst C.
tauto.
apply H2.
eapply between_equality.
2: apply H3.
Between.
apply between_identity in H3.
subst C.
tauto.

prolong A B X A B.
X.
repeat split; try (intro; subst X).
apply bet_col.
assumption.
apply between_identity in H3.
contradiction.
apply cong_symmetry in H4.
apply cong_identity in H4.
contradiction.
apply H0.
eapply between_equality.
apply H3.
Between.
Qed.

Rectangle

Definition Rectangle A B C D := Plg A B C D Cong A C B D.

Lemma Rectangle_Plg : A B C D,
  Rectangle A B C D
  Plg A B C D.
Proof.
unfold Rectangle;tauto.
Qed.

Lemma Rectangle_Parallelogram : A B C D,
  Rectangle A B C D
  Parallelogram A B C D.
Proof.
unfold Rectangle.
intros.
decompose [and] H.
apply plg_to_parallelogram in H0.
auto.
Qed.

Lemma plg_cong_rectangle :
  A B C D,
  Plg A B C D
  Cong A C B D
  Rectangle A B C D.
Proof.
intros.
unfold Rectangle.
tauto.
Qed.


Lemma plg_trivial : A B, A B Parallelogram A B B A.
intros.
right.
unfold Parallelogram_flat.
repeat split; Col; Cong.
Qed.

Lemma plg_trivial1 : A B, A B Parallelogram A A B B.
intros.
right.
unfold Parallelogram_flat.
repeat split; Col; Cong.
Qed.

Lemma col_not_plgs : A B C D, Col A B C ¬Parallelogram_strict A B C D.
intros.
intro.
unfold Parallelogram_strict in H0.
spliter.
unfold TS in H0.
repeat split.
spliter.
apply H0.
Col.
Qed.

Lemma plg_col_plgf : A B C D, Col A B C Parallelogram A B C D Parallelogram_flat A B C D.
intros.
induction H0.
eapply (col_not_plgs A B C D) in H.
contradiction.
assumption.
Qed.

Lemma col_cong_bet : A B C D, Col A B D Cong A B C D Bet A C B Bet C A D Bet C B D.
intros.

prolong B A D1 B C.
prolong A B D2 A C.

assert(Cong A B C D1).
eapply (l2_11 A C B C A D1).
assumption.
eapply between_exchange3.
apply between_symmetry.
apply H1.
assumption.
apply cong_pseudo_reflexivity.
Cong.
assert(D = D1 Midpoint C D D1).
eapply l7_20.
apply bet_col in H1.
apply bet_col in H2.

induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H0.
apply cong_identity in H0.
subst D.
Col.
eapply (col3 A B); Col.

eCong.

induction H7.
subst D1.
left.
eapply between_exchange3.
apply between_symmetry.
apply H1.
assumption.

assert(Cong B A C D2).
eapply (l2_11 B C A C B D2).
Between.
eapply between_exchange3.
apply H1.
assumption.
apply cong_pseudo_reflexivity.
Cong.

assert(Midpoint C D2 D1).
unfold Midpoint.
split.

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H0.
apply cong_identity in H0.
subst D.
apply is_midpoint_id in H7.
subst D1.
Between.
apply between_symmetry.

induction(eq_dec_points B C).
subst C.
apply between_symmetry.
apply cong_identity in H3.
subst D1.
Between.

assert(Bet D1 C B).
eBetween.
assert(Bet C B D2).
eBetween.
eapply (outer_transitivity_between).
apply H11.
assumption.
auto.
unfold Midpoint in H7.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H8.
eapply cong_transitivity.
apply H0.
Cong.
assert(D = D2).
eapply symmetric_point_uniqueness.
apply l7_2.
apply H7.
apply l7_2.
assumption.
subst D2.
right.
eapply between_exchange3.
apply H1.
assumption.
Qed.

Lemma col_cong2_bet1 : A B C D, Col A B D Bet A C B Cong A B C D Cong A C B D Bet C B D.
intros.
induction(eq_dec_points A C).
subst C.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst D.
Between.

assert(HH:=col_cong_bet A B C D H H1 H0).
induction HH.
assert(A = D B = C).
eapply bet_cong_eq.
Between.
eBetween.
Cong.
spliter.
subst D.
subst C.
Between.
assumption.
Qed.

Lemma col_cong2_bet2 : A B C D, Col A B D Bet A C B Cong A B C D Cong A D B C Bet C A D.
intros.

induction(eq_dec_points B C).
subst C.
apply cong_identity in H2.
subst D.
Between.

assert(HH:=col_cong_bet A B C D H H1 H0).
induction HH.
assumption.

assert(C = A D = B).
eapply bet_cong_eq.
Between.
eBetween.
Cong.
spliter.
subst D.
subst C.
Between.
Qed.

Lemma col_cong2_bet3 : A B C D, Col A B D Bet A B C Cong A B C D Cong A C B D Bet B C D.
intros.

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

eapply (col_cong2_bet2 _ A).
apply bet_col in H0.
ColR.
Between.
Cong.
Cong.
Qed.

Lemma col_cong2_bet4 : A B C D, Col A B C Bet A B D Cong A B C D Cong A D B C Bet B D C.
intros.
induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
Between.
apply (col_cong2_bet1 A D B C).
apply bet_col in H0.
ColR.
assumption.
Cong.
Cong.
Qed.

Lemma col_bet2_cong1 : A B C D, Col A B D Bet A C B Cong A B C D Bet C B D Cong A C D B.
intros.
apply (l4_3 A C B D B C); Between; Cong.
Qed.

Lemma col_bet2_cong2 : A B C D, Col A B D Bet A C B Cong A B C D Bet C A D Cong D A B C.
intros.
apply (l4_3 D A C B C A); Between; Cong.
Qed.

Lemma plg_bet1 : A B C D, Parallelogram A B C D Bet A C B Bet D A C.
intros.

apply plg_col_plgf in H.
unfold Parallelogram_flat in H.
spliter.
apply between_symmetry.
apply (col_cong2_bet1 B).
Col.
Between.
Cong.
Cong.
apply bet_col in H0.
Col.
Qed.

Lemma plgf_trivial1 : A B, A B Parallelogram_flat A B B A.
intros.
repeat split; Col; Cong.
Qed.

Lemma plgf_trivial2 : A B, A B Parallelogram_flat A A B B.
intros.
repeat split; Col; Cong.
Qed.

Lemma plgf_not_point : A B, Parallelogram_flat A A B B A B.
intros.
unfold Parallelogram_flat in H.
spliter.
intro.
subst B.
induction H3; tauto.
Qed.

Lemma plgf_trivial_neq : A C D, Parallelogram_flat A A C D C = D A C.
intros.
unfold Parallelogram_flat in H.
spliter.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst D.
split.
reflexivity.
induction H3; auto.
Qed.

Lemma plgf_trivial_trans : A B C, Parallelogram_flat A A B B Parallelogram_flat B B C C
                                            Parallelogram_flat A A C C A = C.
intros.

induction(eq_dec_points A C).
right.
assumption.
left.
unfold Parallelogram_flat in ×.
spliter.
repeat split; Col; Cong.
Qed.


Lemma plgf_trivial : A B, A B Parallelogram_flat A B B A.
intros.
repeat split; Col; Cong.
Qed.

Lemma plgf3_mid : A B C, Parallelogram_flat A B A C Midpoint A B C.
intros.
unfold Parallelogram_flat in H.
spliter.

assert(B=C Midpoint A B C).
eapply l7_20.
Col.
Cong.
induction H3.
tauto.
induction H4.
contradiction.
assumption.
Qed.

Lemma cong3_id : A B C D, A B Col A B C Col A B D Cong A B C D Cong A D B C Cong A C B D
                              A = D B = C A = C B = D.
intros.

induction(eq_dec_points A C).
subst C.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
right.
split; reflexivity.

assert( M, (Midpoint M A B Midpoint M C D) (Midpoint M A D Midpoint M C B)).
apply col_cong_mid.
unfold Par.
right.
repeat split.

assumption.
intro.
subst D.

apply cong_identity in H4.
contradiction.
ColR.
ColR.
intro.
unfold Par_strict in H6.
spliter.
apply H9.
A.
split; Col.
assumption.
ex_and H6 M.

induction H7.

eapply midpoint_cong_uniqueness.
Col.
spliter.
split.
apply H6.
apply l7_2.
assumption.
Cong.

assert(Col A D C).
ColR.

assert(Cong A D C B).
Cong.

assert(HH:= midpoint_cong_uniqueness A D C B M H7 H6 H8).
induction HH.
spliter.
contradiction.
spliter.
contradiction.
Qed.

Lemma col_cong_mid1 : A B C D, A D Col A B C Col A B D Cong A B C D Cong A C B D
                                  M, Midpoint M A D Midpoint M B C.
intros.

assert( M : Tpoint,
       Midpoint M A C Midpoint M B D
       Midpoint M A D Midpoint M B C).

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst D.
assert(HH:=midpoint_existence A C).
ex_and HH M.
M.
left.
tauto.

assert (C D).
intro.
subst D.
apply cong_identity in H2.
contradiction.

apply (col_cong_mid A B C D).
right.
repeat split; Col; ColR.
intro.
unfold Par_strict in H6.
spliter.
apply H9.
C.
split; Col.
assumption.
ex_and H4 M.
induction H5.

assert(A = B C = D A = D C = B).

apply (midpoint_cong_uniqueness A C B D M).
Col.
assumption.
assumption.
induction H5.
spliter.
subst B.
subst D.
M.
tauto.
spliter.
contradiction.
M.
assumption.
Qed.

Lemma col_cong_mid2 : A B C D, A C Col A B C Col A B D Cong A B C D Cong A D B C
                                  M, Midpoint M A C Midpoint M B D.
intros.

assert( M : Tpoint,
       Midpoint M A C Midpoint M B D
       Midpoint M A D Midpoint M B C).

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst D.
assert(HH:=midpoint_existence A C).
ex_and HH M.
M.
left.
tauto.

assert (C D).
intro.
subst D.
apply cong_identity in H2.
contradiction.

apply (col_cong_mid A B C D).
right.
repeat split; Col; ColR.
intro.
unfold Par_strict in H6.
spliter.
apply H9.
C.
split; Col.
assumption.
ex_and H4 M.
induction H5.
M.
assumption.

assert(A = B D = C A = C D = B).

apply (midpoint_cong_uniqueness A D B C M).
Col.
assumption.
assumption.
induction H5.
spliter.
subst B.
subst D.
M.
tauto.
spliter.
contradiction.
Qed.


Lemma plgs_not_col : A B C D, Parallelogram_strict A B C D ¬Col A B C ¬Col A B D.
intros.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.

assert(¬Col A B C).
intro.
apply H.
Col.
split.
assumption.
intro.

induction H0.
unfold Par_strict in H0.
spliter.
apply H8.
D.
split; Col.
spliter.
apply H4.
ColR.
Qed.

Lemma not_col_sym_not_col : A B B' C , ¬Col A B C Midpoint A B B' ¬Col A B' C.
intros.
intro.
apply H.
unfold Midpoint in H0.
spliter.
assert(A B).
intro.
subst B.
apply H.
Col.
assert(A B').
intro.
subst B'.
apply cong_identity in H2.
subst B.
tauto.
apply bet_col in H0.
ColR.
Qed.

Lemma plg_existence : A B C, A B D, Parallelogram A B C D.
intros.
assert(HH:=midpoint_existence A C).
ex_and HH M.
prolong B M D B M.

assert(Midpoint M B D).
unfold Midpoint.
split; Cong.
D.

induction (eq_dec_points A C).
subst C.
apply l7_3 in H0.
subst M.
right.
apply bet_col in H1.
repeat split; Col; Cong.
right.
intro.
subst D.
apply l7_3 in H3.
contradiction.

apply (mid_plg _ _ _ _ M).
left.
assumption.
assumption.
assumption.
Qed.

Lemma plgs_diff : A B C D, Parallelogram_strict A B C D Parallelogram_strict A B C D A B B C C D D A A C B D.
intros.
split.
assumption.
unfold Parallelogram_strict in H.
spliter.
unfold TS in H.
spliter.
repeat split; intro.
subst B.
apply H.
Col.
subst C.
apply H.
Col.
subst D.
apply H2.
Col.
subst D.
apply H2.
Col.
subst C.
apply H.
Col.
subst D.
ex_and H3 T.
apply between_identity in H4.
subst T.
contradiction.
Qed.

Lemma sym_par : A B M, A B A' B', Midpoint M A A' Midpoint M B B' Par A B A' B'.

intros.
eapply (midpoint_par _ _ _ _ M); assumption.
Qed.

Lemma symmetry_preserves_two_sides : A B X Y M A' B', Col X Y M TS X Y A B Midpoint M A A' Midpoint M B B'
                                                TS X Y A' B'.
intros.

assert(X Y ¬Col A X Y ¬Col B X Y).
unfold TS in H0.
spliter.
repeat split; auto.
intro.
subst Y.
Col.
spliter.

assert(A M).
intro.
subst M.
apply H4.
Col.

assert(A' M).
intro.
subst M.
apply H6.
apply sym_equal.
apply is_midpoint_id.
apply l7_2.
assumption.

assert(B M).
intro.
subst M.
apply H5.
Col.

assert(B' M).
intro.
subst M.
apply H8.
apply sym_equal.
apply is_midpoint_id.
apply l7_2.
assumption.

assert(TS X Y A A').
unfold TS.
repeat split; auto.
intro.
apply H4.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.

assert(Col M A' X).
ColR.

assert(Col M A' Y).
ColR.

eapply (col3 A' M); Col.
M.
split.
Col.
apply midpoint_bet.
assumption.

assert(TS X Y B B').
unfold TS.
repeat split; auto.
intro.
apply H5.
unfold Midpoint in H2.
spliter.
apply bet_col in H2.

assert(Col M B' X).
ColR.

assert(Col M B' Y).
ColR.

eapply (col3 B' M); Col.
M.
split.
Col.
apply midpoint_bet.
assumption.

assert(OS X Y A' B).
eapply l9_8_1.
apply l9_2.
apply H10.
apply l9_2.
assumption.
eapply l9_8_2.
apply H11.
apply one_side_symmetry.
assumption.
Qed.

Lemma symmetry_preserves_one_side : A B X Y M A' B', Col X Y M OS X Y A B Midpoint M A A' Midpoint M B B'
                                                OS X Y A' B'.
intros.

assert(X Y ¬Col A X Y ¬Col B X Y).
unfold OS in H0.
ex_and H0 P.
unfold TS in H0.
unfold TS in H3.
spliter.
repeat split; auto.
intro.
subst Y.
Col.
spliter.

assert(A M).
intro.
subst M.
apply H4.
Col.

assert(A' M).
intro.
subst M.
apply H6.
apply sym_equal.
apply is_midpoint_id.
apply l7_2.
assumption.

assert(B M).
intro.
subst M.
apply H5.
Col.

assert(B' M).
intro.
subst M.
apply H8.
apply sym_equal.
apply is_midpoint_id.
apply l7_2.
assumption.

assert(TS X Y A A').
unfold TS.
repeat split; auto.
intro.
apply H4.
unfold Midpoint in H1.
spliter.
apply bet_col in H1.

assert(Col M A' X).
ColR.

assert(Col M A' Y).
ColR.

eapply (col3 A' M); Col.
M.
split.
Col.
apply midpoint_bet.
assumption.

assert(TS X Y B B').
unfold TS.
repeat split; auto.
intro.
apply H5.
unfold Midpoint in H2.
spliter.
apply bet_col in H2.

assert(Col M B' X).
ColR.

assert(Col M B' Y).
ColR.

eapply (col3 B' M); Col.
M.
split.
Col.
apply midpoint_bet.
assumption.
eapply l9_8_1.
apply l9_2.
apply H10.
apply l9_2.

eapply l9_8_2.
apply H11.
apply one_side_symmetry.
assumption.
Qed.

Lemma plgf_bet : A B A' B', Parallelogram_flat A B B' A'
                                  Bet A' B' A Bet B' A B
                                  Bet A' A B' Bet A B' B
                                  Bet A A' B Bet A' B B'
                                  Bet A B A' Bet B A' B'.

intros.
induction H.
spliter.

induction(eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst B'.
left.
split;
Between.

assert(A' B').
intro.
subst B'.
apply cong_identity in H1.
contradiction.

assert(Col A' B' A).
ColR.
assert(Col A' B' B).
ColR.

induction H0.
right; right; right.
split.
assumption.
apply (col_cong2_bet1 A);
Col;
Cong.

induction H0.
right;right; left.
split.
Between.
eapply(col_cong2_bet2 _ A).
Col.
Between.
Cong.
Cong.

induction H.

assert(Bet A' B B').
eapply (outer_transitivity_between2 _ A); auto.

assert(B = B' A' = A).
apply(bet_cong_eq A' A B B' H0 H8).
Cong.
spliter.
subst B'.
subst A'.
right;left.
split; Between.
induction H.

right;left.
split;auto.
eapply (between_inner_transitivity _ _ _ B);
Between.
Between.

induction(eq_dec_points A A').
subst A'.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst B'.
right;left.
split; Between.

left.
split.

assert(Bet A B' A' Bet A A' B').
eapply (l5_2 B).
auto.
Between.
Between.
induction H9.
Between.

assert(Bet B' A' B).
eapply (outer_transitivity_between _ _ A).
Between.
assumption.
auto.

assert(Bet B A' B').
eapply (outer_transitivity_between2 _ A).
Between.
assumption.
assumption.

assert(A = B B' = A').
apply(bet_cong_eq); Between; Cong.
spliter.
contradiction.
assumption.
Qed.

Lemma bet2_cong_bet : A B C D, A B Bet A B C Bet A B D Cong A C B D Bet B C D.
intros.

assert(Bet B C D Bet B D C).
eapply (l5_2 A); auto.
induction H3.
assumption.

assert(D = C A = B).
eapply (bet_cong_eq A B D C); auto.
eBetween.
Cong.
spliter.
contradiction.
Qed.

Lemma not_col_exists : A B, A B P, ¬Col A B P.
intros.
assert(HH:= ex_col2 A B).
ex_and HH C.
assert(HH:=l8_21 A B C H).

ex_and HH P.
ex_and H3 T.
apply perp_not_col in H3.
P.
assumption.
Qed.

Lemma plgs_existence : A B, A B C, D, Parallelogram_strict A B C D.
intros.

assert(HH:=not_col_exists A B H).
ex_and HH C.
assert(HH:=plg_existence A B C H).
ex_and HH D.
C.
D.
induction H1.
assumption.
unfold Parallelogram_flat in H1.
spliter.
contradiction.
Qed.

Lemma Rectangle_not_triv : A,
 ¬ Rectangle A A A A.
Proof.
intros.
unfold Rectangle.
unfold Plg.
intuition.
Qed.

Lemma Rectangle_triv : A B,
 AB
 Rectangle A A B B.
Proof.
intros.
unfold Rectangle.
split;Cong.
unfold Plg.
split.
intuition.
elim (midpoint_existence A B).
intros.
x.
tauto.
Qed.

Lemma Rectangle_not_triv_2 : A B,
 ¬ Rectangle A B A B.
Proof.
intros.
unfold Rectangle.
intro.
spliter.
unfold Plg in H.
intuition.
Qed.

Square

Definition Square A B C D := Rectangle A B C D Cong A B B C.

Lemma Square_not_triv : A,
 ¬ Square A A A A.
Proof.
intros.
unfold Square.
intro.
spliter.
firstorder using Rectangle_not_triv.
Qed.

Lemma Square_not_triv_2 : A B,
 ¬ Square A A B B.
Proof.
intros.
unfold Square.
intro.
spliter.
treat_equalities.
firstorder using Rectangle_not_triv.
Qed.

Lemma Square_not_triv_3 : A B,
 ¬ Square A B A B.
Proof.
intros.
unfold Square.
intro.
spliter.
firstorder using Rectangle_not_triv_2.
Qed.

Lemma Square_Rectangle : A B C D,
 Square A B C D Rectangle A B C D.
Proof.
unfold Square;tauto.
Qed.

Lemma Square_Parallelogram : A B C D,
 Square A B C D Parallelogram A B C D.
Proof.
intros.
apply Square_Rectangle in H.
apply Rectangle_Parallelogram in H.
assumption.
Qed.

Lemma Rhombus_Rectangle_Square : A B C D,
 Rhombus A B C D
 Rectangle A B C D
 Square A B C D.
Proof.
intros.
unfold Square.
unfold Rhombus in ×.
tauto.
Qed.

Lemma rhombus_cong_square : A B C D,
 Rhombus A B C D
 Cong A C B D
 Square A B C D.
Proof.
intros.
apply Rhombus_Rectangle_Square.
assumption.
apply Rhombus_Plg in H.
apply plg_cong_rectangle;auto.
Qed.

Kite

Definition Kite A B C D :=
 Cong B C C D Cong D A A B.

Lemma Kite_comm : A B C D,
 Kite A B C D Kite C D A B.
Proof.
unfold Kite.
tauto.
Qed.

End Quadrilateral.