Require Export GeoCoq.Tarski_dev.Ch03_bet.

Section T3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l4_2 : forall A B C D A' B' C' D', IFSC A B C D A' B' C' D' -> Cong B D B' D'.
Proof.
(* Goal: @IFSC Tn A B C A A' B' C' A' *)
unfold IFSC.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
intros.
(* Goal: @eq (@Tpoint Tn) X B *)
spliter.

(* Goal: @Cong Tn B D B' D' *)
induction (eq_dec_points A C).

(* Goal: @Cong Tn B D B' D' *)
(* Goal: @Cong Tn B D B' D' *)
treat_equalities;assumption.

assert (exists E, Bet A C E /\ C <> E)
 by apply point_construction_different.
(* Goal: @Cong Tn B D B' D' *)
ex_and H6 E.
(* Goal: @Cong Tn B D B' D' *)
prolong A' C' E' C E.

assert  (Cong E D E' D')
 by (
  apply (five_segment_with_def A C E D A' C' E' D');[
  unfold OFSC;  repeat split;Cong|
  assumption]).

(* Goal: @Cong Tn B D B' D' *)
apply (five_segment_with_def E C B D E' C' B' D').
(* Goal: @OFSC Tn E C B D E' C' B' D' *)
(* Goal: not (@eq (@Tpoint Tn) E C) *)
unfold OFSC.
(* Goal: and (@Bet Tn E C B) (and (@Bet Tn E' C' B') (and (@Cong Tn E C E' C') (and (@Cong Tn C B C' B') (and (@Cong Tn E D E' D') (@Cong Tn C D C' D'))))) *)
(* Goal: not (@eq (@Tpoint Tn) E C) *)
repeat split; try solve [eBetween| Cong ].
(* Goal: not (@eq (@Tpoint Tn) E C) *)
auto.
Qed.

Lemma l4_3 : forall A B C A' B' C',
  Bet A B C -> Bet A' B' C' -> Cong A C A' C' -> Cong B C B' C' -> Cong A B A' B'.
Proof.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
intros.
(* Goal: @Cong Tn B C B' C' *)
apply cong_commutativity.
(* Goal: @Cong Tn B A B' A' *)
apply (l4_2 A B C A A' B' C' A').
(* Goal: @IFSC Tn A B C A A' B' C' A' *)
unfold IFSC.
(* Goal: and (@Bet Tn A B C) (and (@Bet Tn A' B' C') (and (@Cong Tn A C A' C') (and (@Cong Tn B C B' C') (and (@Cong Tn A A A' A') (@Cong Tn C A C' A'))))) *)
repeat split;Cong.
Qed.

Lemma l4_3_1 : forall A B C A' B' C',
 Bet A B C -> Bet A' B' C' -> Cong A B A' B' -> Cong A C A' C' -> Cong B C B' C'.
Proof.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
    intros.
(* Goal: @Cong Tn B C B' C' *)
    apply cong_commutativity.
(* Goal: @Cong Tn C B C' B' *)
    eapply l4_3;eBetween;Cong.
Qed.

Lemma l4_5 : forall A B C A' C',
  Bet A B C -> Cong A C A' C' ->
  exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'.
Proof.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
intros.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A X C), @eq (@Tpoint Tn) X B *)
unfold Cong_3.

assert (exists D', Bet C' A' D' /\ A' <> D')
 by (apply point_construction_different).
ex_and H1 x'.
prolong x' A' B' A B.
prolong x' B' C'' B C.

assert (Bet A' B' C'') by eBetween.

assert (C'' = C').
eapply (construction_uniqueness x' A' ).

(* Goal: not (@eq (@Tpoint Tn) E C) *)
auto.
eBetween.

apply (l2_11 A' B' C'' A B C);Between.

eBetween.
Cong.

subst C''.
exists B'.
(* Goal: and (@Bet Tn A B C) (and (@Bet Tn A' B' C') (and (@Cong Tn A C A' C') (and (@Cong Tn B C B' C') (and (@Cong Tn A A A' A') (@Cong Tn C A C' A'))))) *)
repeat split;Cong.
Qed.

Lemma l4_6 : forall A B C A' B' C', Bet A B C -> Cong_3 A B C A' B' C' -> Bet A' B' C'.
Proof.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A X C), @eq (@Tpoint Tn) X B *)
unfold Cong_3.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
intros.
assert (exists B'', Bet A' B'' C' /\ Cong_3 A B C A' B'' C')
  by (eapply l4_5;intuition).
(* Goal: @Bet Tn A' B' C' *)
ex_and H1 x.
(* Goal: @eq (@Tpoint Tn) X B *)
unfold Cong_3 in *;spliter.

(* Goal: @Bet Tn A' B' C' *)
assert (Cong_3 A' x C' A' B' C').
  unfold Cong_3;repeat split; Cong.
  apply cong_transitivity with A B; Cong.
  apply cong_transitivity with B C; Cong.
(* Goal: @eq (@Tpoint Tn) X B *)
unfold Cong_3 in H7;spliter.

assert (IFSC A' x C' x  A' x C' B')
 by (unfold IFSC;repeat split;Cong).
assert (Cong x x x B')
 by (eapply l4_2;apply H10).
(* Goal: @eq (@Tpoint Tn) X B *)
Between.
Qed.

Lemma cong3_bet_eq : forall  A B C X,
 Bet A B C -> Cong_3 A B C A X C -> X = B.
Proof.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Cong_3 Tn A B C A X C), @eq (@Tpoint Tn) X B *)
unfold Cong_3.
(* Goal: forall (A B C X : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : and (@Cong Tn A B A X) (and (@Cong Tn A C A C) (@Cong Tn B C X C))), @eq (@Tpoint Tn) X B *)
intros.
(* Goal: @eq (@Tpoint Tn) X B *)
spliter.
assert (IFSC A B C B A B C X)
 by (unfold IFSC;intuition).
assert (Cong B B B X)
 by (apply (l4_2 _ _ _ _ _ _ _ _ H3)).
(* Goal: @eq (@Tpoint Tn) X B *)
Between.
Qed.

End T3.
