Library bet_le
Require Export col.
Section T5.
Context `{M:Tarski}.
Ltac assert_cols :=
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)
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
end.
Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
match goal with
| H:(?X1 = ?X2) |- _ => smart_subst X2
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.
Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].
Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.
Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition IFSC := fun 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'.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Lemma l5_1 : forall A B C D,
A<>B -> Bet A B C -> Bet A B D -> Bet A C D \/ Bet A D C.
Proof.
intros.
prolong A D C' C D.
prolong A C D' C D.
prolong A C' B' C B.
prolong A D' B'' D B.
assert (Cong B C' B'' C)
by (apply (l2_l1 B D C' B'' D' C);eBetween;eCong).
assert (Cong B B' B'' B)
by (apply (l2_l1 B C' B' B'' C B);eBetween;eCong).
assert(B'' = B') by
(eapply (construction_unicity A B _ _ _ _ H);
eBetween; eCong).
subst B''.
assert (FSC B C D' C' B' C' D C).
unfold FSC.
repeat split.
unfold Col.
eBetween.
Cong.
2:eCong.
2:assumption.
2:apply cong_pseudo_reflexivity.
eapply (l2_l1 B _ D' B' _ D).
eapply between_exchange3.
2:apply H4.
assumption.
apply between_symmetry.
eapply between_exchange3.
2:apply H6.
assumption.
induction (eq_dec_points B C).
subst C.
Cong.
Cong.
eCong.
induction (eq_dec_points B C).
subst C.
auto.
assert (Cong D' C' D C) by
(eapply l4_16; try apply H12; assumption).
assert (exists E, Bet C E C' /\ Bet D E D') by
(eapply inner_pasch;eBetween).
ex_and H15 E.
assert (IFSC D E D' C D E D' C') by
(unfold IFSC;repeat split;eCong).
assert (IFSC C E C' D C E C' D') by
(unfold IFSC;repeat split;eCong).
assert (Cong E C E C') by
(eapply l4_2;apply H17).
assert (Cong E D E D') by
(eapply l4_2;apply H18).
induction (eq_dec_points C C').
subst C'.
right.
assumption.
show_distinct C D';intuition.
prolong C' C P C D'.
prolong D' C R C E.
prolong P R Q R P.
assert (FSC D' C R P P C E D').
unfold FSC.
unfold Cong_3.
repeat split.
4:assumption.
unfold Col;auto.
Cong.
eapply (l2_l1 D' C R).
apply H25.
4: apply cong_pseudo_reflexivity.
3:apply H26.
3:assumption.
eBetween.
Cong.
assert (Cong R P E D').
eauto using l4_16.
assert (Cong R Q E D)
by (eapply cong_transitivity;eCong).
assert (FSC D' E D C P R Q C).
unfold FSC.
repeat split.
unfold Col.
Between.
Cong.
2:Cong.
3:Cong.
eapply (l2_l1 D' E D P R Q);eBetween;eCong.
Cong.
assert (Cong D C Q C).
induction (eq_dec_points D' E).
unfold FSC, IFSC, Cong_3 in *;spliter.
treat_equalities.
Cong.
eapply l4_16.
apply H32.
assumption.
assert (Cong C P C Q).
unfold FSC in *;unfold Cong_3 in *.
spliter.
eCong.
show_distinct R C.
intuition.
assert (Cong D' P D' Q)
by (apply (l4_17 R C);unfold Col;Between;Cong).
assert (Cong B P B Q).
eapply l4_17.
unfold not;apply H22.
unfold Col.
right;right.
eapply between_exchange3.
apply H0.
assumption.
assumption.
assumption.
assert (Cong B' P B' Q).
eapply (l4_17 C D').
auto.
unfold Col.
left.
eapply between_exchange3.
apply H4.
assumption.
assumption.
assumption.
assert (Cong C' P C' Q).
induction(eq_dec_points B B').
Focus 2.
eapply l4_17.
apply H39.
unfold Col.
right;left.
apply between_symmetry.
eapply between_exchange3.
2:apply H6.
eapply between_exchange4.
2:apply H2.
assumption.
assumption.
assumption.
subst B'.
unfold IFSC,FSC, Cong_3 in *.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
eapply l4_17.
unfold not;apply H22.
unfold Col.
left.
eapply between_exchange3.
apply H4.
eapply between_exchange4.
apply H8.
eapply between_exchange4.
apply H1.
assumption.
assumption.
assumption.
assert (Cong P P P Q).
eapply l4_17.
unfold not;apply H21.
unfold Col.
right;right.
apply between_symmetry.
assumption.
assumption.
assumption.
unfold IFSC,FSC, Cong_3 in *;spliter.
treat_equalities.
Between.
Qed.
Lemma l5_2 : forall A B C D,
A<>B -> Bet A B C -> Bet A B D -> Bet B C D \/ Bet B D C.
Proof.
intros.
assert (Bet A C D \/ Bet A D C) by
(eapply l5_1;eauto).
induction H2;
eBetween.
Qed.
Lemma l5_3 : forall A B C D,
Bet A B D -> Bet A C D -> Bet A B C \/ Bet A C B.
Proof.
intros.
assert (exists P, Bet D A P /\ A<>P) by
(apply point_construction_different).
ex_and H1 P.
assert (Bet P A B) by eBetween.
assert (Bet P A C) by eBetween.
apply (l5_2 P);auto.
Qed.
Definition le := fun A B C D =>
exists y, Bet C y D /\ Cong A B C y.
Definition ge := fun A B C D => le C D A B.
Lemma l5_5_1 : forall A B C D,
le A B C D -> exists x, Bet A B x /\ Cong A x C D.
Proof.
unfold le.
intros.
ex_and H P.
prolong A B x P D.
exists x.
split.
assumption.
eapply l2_l1;eauto.
Qed.
Lemma l5_5_2 : forall A B C D,
(exists x, Bet A B x /\ Cong A x C D) -> le A B C D.
Proof.
intros.
ex_and H P.
unfold le.
assert (exists B' : Tpoint, Bet C B' D /\ Cong_3 A B P C B' D)
by (eapply l4_5;auto).
ex_and H1 y.
exists y.
unfold Cong_3 in *;intuition.
Qed.
Lemma l5_6 : forall A B C D A' B' C' D',
le A B C D /\ Cong A B A' B' /\ Cong C D C' D' -> le A' B' C' D'.
Proof.
unfold le.
intros.
spliter.
ex_and H y.
assert (exists z : Tpoint, Bet C' z D' /\ Cong_3 C y D C' z D')
by (eapply l4_5;auto).
ex_and H3 z.
exists z.
split.
assumption.
unfold Cong_3 in *;spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H0.
eapply cong_transitivity.
apply H2.
assumption.
Qed.
Lemma le_reflexivity : forall A B, le A B A B.
Proof.
unfold le.
intros.
exists B.
split;Between;Cong.
Qed.
Lemma le_transitivity : forall A B C D E F, le A B C D -> le C D E F -> le A B E F .
Proof.
unfold le.
intros.
ex_and H y.
ex_and H0 z.
assert (exists P : Tpoint, Bet E P z /\ Cong_3 C y D E P z)
by (eapply l4_5;assumption).
ex_and H3 P.
exists P.
split.
eBetween.
unfold Cong_3 in H4;spliter;eCong.
Qed.
Lemma between_cong : forall A B C, Bet A C B -> Cong A C A B -> C=B.
Proof.
intros.
assert (Bet A B C).
eapply l4_6.
apply H.
unfold Cong_3.
repeat split;Cong.
eapply between_egality;eBetween.
Qed.
Lemma cong3_symmetry : forall A B C A' B' C' : Tpoint , Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
unfold Cong_3.
intros.
intuition.
Qed.
Lemma between_cong_2 : forall A B D E, Bet A D B -> Bet A E B -> Cong A D A E -> D = E.
Proof.
intros.
assert (Bet A D E \/ Bet A E D)
by (apply (l5_3 A D _ B);auto).
induction H2.
eapply between_cong.
apply H2.
assumption.
eapply between_cong.
2:apply H1.
assert (Cong_3 A E D A D E)
by (unfold Cong_3;repeat split;Cong).
eapply l4_6;eauto.
Qed.
Lemma between_cong_2' : forall A B D E, Bet A D B -> Bet A E B -> Cong A D A E -> D = E.
Proof.
intros.
eapply cong3_bet_eq.
apply H0.
unfold Cong_3.
repeat split;Cong.
eapply (l4_2 B E A B B D A B).
unfold IFSC;repeat split;Cong;Between.
Qed.
Lemma le_anti_symmetry : forall A B C D, le A B C D -> le C D A B -> Cong A B C D.
Proof.
intros.
assert (exists T, Bet C D T /\ Cong C T A B)
by (apply l5_5_1;assumption).
unfold le in H.
ex_and H Y.
ex_and H1 T.
assert (Cong C Y C T) by eCong.
assert (Bet C Y T) by eBetween.
assert (Y=T) by (eapply between_cong;eauto).
subst Y.
assert (T=D) by (eapply between_egality;eBetween).
subst T.
Cong.
Qed.
Lemma segment_construction_2 : forall A Q B C, A<>Q -> exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C.
Proof.
intros.
prolong A Q A' A Q.
prolong A' Q X B C.
exists X.
show_distinct A' Q.
solve [intuition].
split.
eapply (l5_2 A' Q);Between.
assumption.
Qed.
Lemma le_trivial : forall A C D, le A A C D .
Proof.
intros.
unfold le.
exists C.
split;Between;Cong.
Qed.
Lemma le_cases : forall A B C D, le A B C D \/ le C D A B.
Proof.
intros.
induction(eq_dec_points A B).
subst B.
left.
apply le_trivial.
assert (exists X : Tpoint, (Bet A B X \/ Bet A X B) /\ Cong A X C D) by
(eapply (segment_construction_2 B A C D);auto).
ex_and H0 X.
induction H0.
left.
apply l5_5_2.
exists X.
split;assumption.
right.
unfold le.
exists X.
split;Cong.
Qed.
Lemma le_zero : forall A B C, le A B C C -> A=B.
Proof.
intros.
assert (le C C A B)
by apply le_trivial.
assert (Cong A B C C) by
(apply le_anti_symmetry;assumption).
treat_equalities;auto.
Qed.
Definition lt := fun A B C D => le A B C D /\ ~ Cong A B C D.
Definition gt := fun A B C D => lt C D A B.
End T5.
Section T5.
Context `{M:Tarski}.
Ltac assert_cols :=
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)
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
end.
Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
match goal with
| H:(?X1 = ?X2) |- _ => smart_subst X2
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.
Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].
Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.
Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition IFSC := fun 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'.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Lemma l5_1 : forall A B C D,
A<>B -> Bet A B C -> Bet A B D -> Bet A C D \/ Bet A D C.
Proof.
intros.
prolong A D C' C D.
prolong A C D' C D.
prolong A C' B' C B.
prolong A D' B'' D B.
assert (Cong B C' B'' C)
by (apply (l2_l1 B D C' B'' D' C);eBetween;eCong).
assert (Cong B B' B'' B)
by (apply (l2_l1 B C' B' B'' C B);eBetween;eCong).
assert(B'' = B') by
(eapply (construction_unicity A B _ _ _ _ H);
eBetween; eCong).
subst B''.
assert (FSC B C D' C' B' C' D C).
unfold FSC.
repeat split.
unfold Col.
eBetween.
Cong.
2:eCong.
2:assumption.
2:apply cong_pseudo_reflexivity.
eapply (l2_l1 B _ D' B' _ D).
eapply between_exchange3.
2:apply H4.
assumption.
apply between_symmetry.
eapply between_exchange3.
2:apply H6.
assumption.
induction (eq_dec_points B C).
subst C.
Cong.
Cong.
eCong.
induction (eq_dec_points B C).
subst C.
auto.
assert (Cong D' C' D C) by
(eapply l4_16; try apply H12; assumption).
assert (exists E, Bet C E C' /\ Bet D E D') by
(eapply inner_pasch;eBetween).
ex_and H15 E.
assert (IFSC D E D' C D E D' C') by
(unfold IFSC;repeat split;eCong).
assert (IFSC C E C' D C E C' D') by
(unfold IFSC;repeat split;eCong).
assert (Cong E C E C') by
(eapply l4_2;apply H17).
assert (Cong E D E D') by
(eapply l4_2;apply H18).
induction (eq_dec_points C C').
subst C'.
right.
assumption.
show_distinct C D';intuition.
prolong C' C P C D'.
prolong D' C R C E.
prolong P R Q R P.
assert (FSC D' C R P P C E D').
unfold FSC.
unfold Cong_3.
repeat split.
4:assumption.
unfold Col;auto.
Cong.
eapply (l2_l1 D' C R).
apply H25.
4: apply cong_pseudo_reflexivity.
3:apply H26.
3:assumption.
eBetween.
Cong.
assert (Cong R P E D').
eauto using l4_16.
assert (Cong R Q E D)
by (eapply cong_transitivity;eCong).
assert (FSC D' E D C P R Q C).
unfold FSC.
repeat split.
unfold Col.
Between.
Cong.
2:Cong.
3:Cong.
eapply (l2_l1 D' E D P R Q);eBetween;eCong.
Cong.
assert (Cong D C Q C).
induction (eq_dec_points D' E).
unfold FSC, IFSC, Cong_3 in *;spliter.
treat_equalities.
Cong.
eapply l4_16.
apply H32.
assumption.
assert (Cong C P C Q).
unfold FSC in *;unfold Cong_3 in *.
spliter.
eCong.
show_distinct R C.
intuition.
assert (Cong D' P D' Q)
by (apply (l4_17 R C);unfold Col;Between;Cong).
assert (Cong B P B Q).
eapply l4_17.
unfold not;apply H22.
unfold Col.
right;right.
eapply between_exchange3.
apply H0.
assumption.
assumption.
assumption.
assert (Cong B' P B' Q).
eapply (l4_17 C D').
auto.
unfold Col.
left.
eapply between_exchange3.
apply H4.
assumption.
assumption.
assumption.
assert (Cong C' P C' Q).
induction(eq_dec_points B B').
Focus 2.
eapply l4_17.
apply H39.
unfold Col.
right;left.
apply between_symmetry.
eapply between_exchange3.
2:apply H6.
eapply between_exchange4.
2:apply H2.
assumption.
assumption.
assumption.
subst B'.
unfold IFSC,FSC, Cong_3 in *.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
eapply l4_17.
unfold not;apply H22.
unfold Col.
left.
eapply between_exchange3.
apply H4.
eapply between_exchange4.
apply H8.
eapply between_exchange4.
apply H1.
assumption.
assumption.
assumption.
assert (Cong P P P Q).
eapply l4_17.
unfold not;apply H21.
unfold Col.
right;right.
apply between_symmetry.
assumption.
assumption.
assumption.
unfold IFSC,FSC, Cong_3 in *;spliter.
treat_equalities.
Between.
Qed.
Lemma l5_2 : forall A B C D,
A<>B -> Bet A B C -> Bet A B D -> Bet B C D \/ Bet B D C.
Proof.
intros.
assert (Bet A C D \/ Bet A D C) by
(eapply l5_1;eauto).
induction H2;
eBetween.
Qed.
Lemma l5_3 : forall A B C D,
Bet A B D -> Bet A C D -> Bet A B C \/ Bet A C B.
Proof.
intros.
assert (exists P, Bet D A P /\ A<>P) by
(apply point_construction_different).
ex_and H1 P.
assert (Bet P A B) by eBetween.
assert (Bet P A C) by eBetween.
apply (l5_2 P);auto.
Qed.
Definition le := fun A B C D =>
exists y, Bet C y D /\ Cong A B C y.
Definition ge := fun A B C D => le C D A B.
Lemma l5_5_1 : forall A B C D,
le A B C D -> exists x, Bet A B x /\ Cong A x C D.
Proof.
unfold le.
intros.
ex_and H P.
prolong A B x P D.
exists x.
split.
assumption.
eapply l2_l1;eauto.
Qed.
Lemma l5_5_2 : forall A B C D,
(exists x, Bet A B x /\ Cong A x C D) -> le A B C D.
Proof.
intros.
ex_and H P.
unfold le.
assert (exists B' : Tpoint, Bet C B' D /\ Cong_3 A B P C B' D)
by (eapply l4_5;auto).
ex_and H1 y.
exists y.
unfold Cong_3 in *;intuition.
Qed.
Lemma l5_6 : forall A B C D A' B' C' D',
le A B C D /\ Cong A B A' B' /\ Cong C D C' D' -> le A' B' C' D'.
Proof.
unfold le.
intros.
spliter.
ex_and H y.
assert (exists z : Tpoint, Bet C' z D' /\ Cong_3 C y D C' z D')
by (eapply l4_5;auto).
ex_and H3 z.
exists z.
split.
assumption.
unfold Cong_3 in *;spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H0.
eapply cong_transitivity.
apply H2.
assumption.
Qed.
Lemma le_reflexivity : forall A B, le A B A B.
Proof.
unfold le.
intros.
exists B.
split;Between;Cong.
Qed.
Lemma le_transitivity : forall A B C D E F, le A B C D -> le C D E F -> le A B E F .
Proof.
unfold le.
intros.
ex_and H y.
ex_and H0 z.
assert (exists P : Tpoint, Bet E P z /\ Cong_3 C y D E P z)
by (eapply l4_5;assumption).
ex_and H3 P.
exists P.
split.
eBetween.
unfold Cong_3 in H4;spliter;eCong.
Qed.
Lemma between_cong : forall A B C, Bet A C B -> Cong A C A B -> C=B.
Proof.
intros.
assert (Bet A B C).
eapply l4_6.
apply H.
unfold Cong_3.
repeat split;Cong.
eapply between_egality;eBetween.
Qed.
Lemma cong3_symmetry : forall A B C A' B' C' : Tpoint , Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
unfold Cong_3.
intros.
intuition.
Qed.
Lemma between_cong_2 : forall A B D E, Bet A D B -> Bet A E B -> Cong A D A E -> D = E.
Proof.
intros.
assert (Bet A D E \/ Bet A E D)
by (apply (l5_3 A D _ B);auto).
induction H2.
eapply between_cong.
apply H2.
assumption.
eapply between_cong.
2:apply H1.
assert (Cong_3 A E D A D E)
by (unfold Cong_3;repeat split;Cong).
eapply l4_6;eauto.
Qed.
Lemma between_cong_2' : forall A B D E, Bet A D B -> Bet A E B -> Cong A D A E -> D = E.
Proof.
intros.
eapply cong3_bet_eq.
apply H0.
unfold Cong_3.
repeat split;Cong.
eapply (l4_2 B E A B B D A B).
unfold IFSC;repeat split;Cong;Between.
Qed.
Lemma le_anti_symmetry : forall A B C D, le A B C D -> le C D A B -> Cong A B C D.
Proof.
intros.
assert (exists T, Bet C D T /\ Cong C T A B)
by (apply l5_5_1;assumption).
unfold le in H.
ex_and H Y.
ex_and H1 T.
assert (Cong C Y C T) by eCong.
assert (Bet C Y T) by eBetween.
assert (Y=T) by (eapply between_cong;eauto).
subst Y.
assert (T=D) by (eapply between_egality;eBetween).
subst T.
Cong.
Qed.
Lemma segment_construction_2 : forall A Q B C, A<>Q -> exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C.
Proof.
intros.
prolong A Q A' A Q.
prolong A' Q X B C.
exists X.
show_distinct A' Q.
solve [intuition].
split.
eapply (l5_2 A' Q);Between.
assumption.
Qed.
Lemma le_trivial : forall A C D, le A A C D .
Proof.
intros.
unfold le.
exists C.
split;Between;Cong.
Qed.
Lemma le_cases : forall A B C D, le A B C D \/ le C D A B.
Proof.
intros.
induction(eq_dec_points A B).
subst B.
left.
apply le_trivial.
assert (exists X : Tpoint, (Bet A B X \/ Bet A X B) /\ Cong A X C D) by
(eapply (segment_construction_2 B A C D);auto).
ex_and H0 X.
induction H0.
left.
apply l5_5_2.
exists X.
split;assumption.
right.
unfold le.
exists X.
split;Cong.
Qed.
Lemma le_zero : forall A B C, le A B C C -> A=B.
Proof.
intros.
assert (le C C A B)
by apply le_trivial.
assert (Cong A B C C) by
(apply le_anti_symmetry;assumption).
treat_equalities;auto.
Qed.
Definition lt := fun A B C D => le A B C D /\ ~ Cong A B C D.
Definition gt := fun A B C D => lt C D A B.
End T5.