Library col

Require Export cong_bet.

Section T4.

Context `{M:Tarski}.


Lemma col_permutation_1 : forall A B C,Col A B C -> Col B C A.
Proof.
unfold Col.
intros.
intuition.
Qed.

Lemma col_permutation_2 : forall A B C, Col A B C -> Col C A B.
Proof.
unfold Col.
intros.
intuition.
Qed.

Lemma col_permutation_3 : forall A B C, Col A B C -> Col C B A.
Proof.
unfold Col.
intros.
intuition.
Qed.

Lemma col_permutation_4 : forall A B C, Col A B C -> Col B A C.
Proof.
unfold Col.
intros.
intuition.
Qed.

Lemma col_permutation_5 : forall A B C, Col A B C -> Col A C B.
Proof.
unfold Col.
intros.
intuition.
Qed.

Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.

Ltac Col := auto with Col.
Ltac eCol := eauto with Col.

Lemma col_trivial_1 : forall A B, Col A A B.
Proof.
unfold Col.
intros.
Between.
Qed.

Lemma col_trivial_2 : forall A B, Col A B B.
Proof.
unfold Col.
intros.
Between.
Qed.

Lemma col_trivial_3 : forall A B, Col A B A.
Proof.
unfold Col.
intros.
Between.
Qed.

Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.

Lemma l4_13 : forall A B C A' B' C',
 Col A B C -> Cong_3 A B C A' B' C' -> Col A' B' C'.
Proof.
unfold Col.
intros.
decompose [or] H.

left.
eauto using l4_6.

right;left.
eapply l4_6;eauto with Cong3.

right;right.
eapply l4_6;eauto with Cong3.
Qed.

Lemma l4_14 : forall A B C A' B',
  Col A B C -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C'.
Proof.
unfold Col.
intros.
intuition.

prolong A' B' C' B C.
exists C'.
assert (Cong A C A' C') by (eapply l2_l1;eCong).

unfold Cong_3;intuition.

assert (exists C', Bet A' C' B' /\ Cong_3 A C B A' C' B')
 by (eapply l4_5;Between).
ex_and H1 C'.
exists C'.
auto with Cong3.

prolong B' A' C' A C.
exists C'.
assert (Cong B C B' C')
 by (eapply l2_l1;eBetween;Cong).
unfold Cong_3;intuition.
Qed.

Definition FSC := fun A B C D A' B' C' D' =>
  Col A B C /\ Cong_3 A B C A' B' C' /\ Cong A D A' D' /\ Cong B D B' D'.

Lemma l4_16 : forall A B C D A' B' C' D',
   FSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
unfold FSC.
unfold Col.
intros.
decompose [or and] H; clear H.
assert (Bet A' B' C')
 by (eapply l4_6;eauto).
unfold Cong_3 in *;spliter.

assert(OFSC A B C D A' B' C' D')
 by (unfold OFSC;repeat split; try assumption).

eapply five_segments_with_def;eauto.

assert(Bet B' C' A')
 by (apply (l4_6 B C A B' C' A');Cong;auto with Cong3).

apply (l4_2 B C A D B' C' A' D').
unfold IFSC;unfold Cong_3 in *;spliter;
repeat split;Between;Cong.

assert (Bet C' A' B') by
 (eapply (l4_6 C A B C' A' B');auto with Cong3).

eapply (five_segments_with_def B A C D B' A');
unfold OFSC;unfold Cong_3 in *;spliter;
repeat split;Between;Cong.
Qed.

Lemma l4_17 : forall A B C P Q, A<>B -> Col A B C -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q.
Proof.
intros.
assert (FSC A B C P A B C Q) by
 (unfold FSC;unfold Cong_3;Cong).
eapply l4_16;eauto.
Qed.

Lemma l4_18 : forall A B C C',
  A<>B -> Col A B C -> Cong A C A C' -> Cong B C B C' -> C=C'.
Proof.
intros.
eapply cong_identity.
apply (l4_17 A B);Cong.
Qed.

Lemma l4_19 : forall A B C C',
 Bet A C B -> Cong A C A C' -> Cong B C B C' -> C=C'.
Proof.
intros.
induction (eq_dec_points A B).
treat_equalities;reflexivity.

apply (l4_18 A B);Cong.
auto using bet_col with Col.
Qed.

End T4.