Library GeoCoq.Tarski_dev.Ch04_cong_bet

Require Export GeoCoq.Tarski_dev.Ch03_bet.

Section T3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition IFSC A B C D A' B' C' D' :=
   Bet A B C Bet A' B' C'
   Cong A C A' C' Cong B C B' C'
   Cong A D A' D' Cong C D C' D'.

Lemma l4_2 : A B C D A' B' C' D', IFSC A B C D A' B' C' D' Cong B D B' D'.
Proof.
unfold IFSC.
intros.
spliter.

induction (eq_dec_points A C).

treat_equalities;assumption.

assert ( E, Bet A C E C E)
 by apply point_construction_different.
ex_and H6 E.
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]).

apply (five_segment_with_def E C B D E' C' B' D').
unfold OFSC.
repeat split; try solve [eBetween| Cong ].
auto.
Qed.

Lemma l4_3 : 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.
intros.
apply cong_commutativity.
apply (l4_2 A B C A A' B' C' A').
unfold IFSC.
repeat split;Cong.
Qed.

Lemma l4_3_1 : 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.
    intros.
    apply cong_commutativity.
    eapply l4_3;eBetween;Cong.
Qed.

Lemma l4_5 : A B C A' C',
  Bet A B C Cong A C A' C'
   B', Bet A' B' C' Cong_3 A B C A' B' C'.
Proof.
intros.
unfold Cong_3.

assert ( 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' ).

auto.
eBetween.

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

eBetween.
Cong.

subst C''.
B'.
repeat split;Cong.
Qed.

Lemma l4_6 : A B C A' B' C', Bet A B C Cong_3 A B C A' B' C' Bet A' B' C'.
Proof.
unfold Cong_3.
intros.
assert ( B'', Bet A' B'' C' Cong_3 A B C A' B'' C')
  by (eapply l4_5;intuition).
ex_and H1 x.
unfold Cong_3 in *;spliter.

assert (Cong_3 A' x C' A' B' C')
 by (unfold Cong_3;repeat split;eCong).
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).
Between.
Qed.

Lemma cong3_bet_eq : A B C X,
 Bet A B C Cong_3 A B C A X C X = B.
Proof.
unfold Cong_3.
intros.
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)).
Between.
Qed.

End T3.