Library plane
Require Export orthogonality.
Section T9.
Context `{MT: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.
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.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Ltac double A B A' :=
assert (mp:= mdp A B);
elim mp; intros A' ; intro; clear mp.
Definition two_sides := fun A B P Q =>
A<>B /\ ~ Col P A B /\ ~ Col Q A B /\ exists T, Col T A B /\ Bet P T Q.
Lemma l9_2 : forall A B P Q, two_sides A B P Q -> two_sides A B Q P.
unfold two_sides.
intros.
spliter.
repeat split;try assumption.
ex_and H2 T.
exists T.
split;
Between.
Qed.
Lemma inter_unicity : forall A B X Y M N, Col A B M-> Col X Y M -> Col A B N -> Col X Y N ->
~ Col A X B -> X <> Y -> M = N.
intros.
eapply l6_21.
3:apply H.
4: apply H0.
intro.
apply H3.
apply col_permutation_5.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma col2 : forall A B X Y, A <> B -> Col A B X -> Col A B Y -> Col A X Y.
intros.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
Qed.
Lemma colx : forall A B M N X, A <> B -> N <> M -> X <> M -> Col A B M -> Col A B N -> Col M N X -> Col A B X.
intros.
assert (Col A M N).
eapply col2.
apply H.
assumption.
assumption.
assert(Col B M N).
eapply (col2 B A).
auto.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
assert (Col M A X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.
assert(Col M B X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.
apply col_permutation_2 in H6.
apply col_permutation_2 in H7.
apply col_permutation_1.
eapply (col2).
apply H1.
assumption.
apply col_permutation_2.
assumption.
Qed.
Lemma l9_3 : forall P Q A C M R B,
two_sides P Q A C -> Col M P Q ->
is_midpoint M A C -> Col R P Q ->
out R A B -> two_sides P Q B C.
Proof.
intros.
unfold two_sides in *.
spliter.
ex_and H6 T.
assert (A <> C).
intro.
subst C.
eapply l7_3 in H1.
subst M.
apply H4.
assumption.
assert (T = M).
eapply inter_unicity.
apply col_permutation_1.
apply H6.
unfold Col.
right; left.
apply H7.
apply col_permutation_1.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
auto.
subst T.
repeat split.
assumption.
2:assumption.
induction(eq_dec_points C M).
subst M.
intro.
apply H5.
assumption.
intro.
clear H0.
assert (B <> R).
intro.
subst B.
unfold out in H3.
spliter.
absurde.
assert (Col P R B).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col P R A).
induction (eq_dec_points P B).
subst B.
unfold out in H3.
spliter.
induction H13.
unfold Col.
right; left.
apply H13.
unfold Col.
right; right.
apply between_symmetry.
assumption.
apply col_permutation_2.
eapply col_transitivity_2.
apply H0.
unfold Col.
unfold out in H3.
spliter.
induction H14.
right; left.
assumption.
right; right.
apply between_symmetry.
assumption.
apply col_permutation_3.
assumption.
induction (eq_dec_points P R).
subst R.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ B).
unfold out in H3.
spliter.
auto.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H14.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
assert (Col P B A ).
eapply col_transitivity_1.
apply H13.
assumption.
assumption.
induction (eq_dec_points P B).
subst B.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ R).
apply H0.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H16.
right; left.
assumption.
right;right.
apply between_symmetry.
assumption.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H15.
apply col_permutation_4.
assumption.
assumption.
induction H3.
spliter.
induction H10.
Focus 2.
assert (exists X, Bet B X C /\ Bet M X R).
eapply inner_pasch.
apply H10.
apply between_symmetry.
assumption.
ex_and H11 X.
exists X.
induction (eq_dec_points M R).
subst R.
apply between_identity in H12.
subst X.
split; assumption.
induction (eq_dec_points R X).
subst X.
split; assumption.
split.
induction (eq_dec_points X M).
subst X.
assumption.
assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col X P Q).
apply col_permutation_2.
eapply colx.
assumption.
apply H13.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
assumption.
assumption.
assumption.
double B M B'.
double R M R'.
assert (Bet B' C R').
eapply l7_15.
apply H11.
apply H1.
apply H12.
apply between_symmetry.
assumption.
assert (exists X, Bet M X R' /\ Bet C X B).
eapply inner_pasch.
apply mid_bet.
apply H11.
apply between_symmetry.
assumption.
ex_and H14 X.
exists X.
split.
assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col Q M R).
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.
induction (eq_dec_points M X).
subst X.
assumption.
induction (eq_dec_points M R').
subst R'.
apply between_identity in H14.
subst X.
absurde.
assert (M <> R).
intro.
subst R.
eapply (midpoint_id) in H12.
apply H19.
apply H12.
apply l7_3_2.
apply col_permutation_2.
eapply (colx _ _ M R).
assumption.
auto.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
eapply (col_transitivity_1).
apply H20.
apply col_trivial_2.
eapply col_transitivity_1.
apply H19.
unfold Col.
right; right.
apply mid_bet.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
Qed.
Definition is_symmetric (A A' C : Tpoint) := is_midpoint C A A'.
Lemma sym_sym : forall A C A', is_symmetric A A' C -> is_symmetric A' A C.
unfold is_symmetric.
intros.
apply l7_2.
assumption.
Qed.
Lemma distinct : forall P Q R : Tpoint, P <> Q -> (R <> P \/ R <> Q).
Proof.
intros.
assert (~ (R = P /\ R = Q) -> (R <> P \/ R <> Q)).
intro.
induction (eq_dec_points P R).
subst R.
right.
intro.
apply H0.
split.
reflexivity.
assumption.
left.
intro.
apply H1.
subst R.
reflexivity.
apply H0.
intro.
spliter.
subst P.
subst Q.
apply H.
reflexivity.
Qed.
Lemma diff_col_ex : forall A B, exists C, A <> C /\ B <> C /\ Col A B C.
intros.
assert (exists C, Bet A B C /\ B <> C).
apply point_construction_different.
ex_and H C.
exists C.
split.
intro.
induction (eq_dec_points A B).
subst B.
subst C.
apply H0.
reflexivity.
subst C.
apply between_identity in H.
subst B.
apply H0.
reflexivity.
split.
assumption.
unfold Col.
left.
assumption.
Qed.
Lemma diff_bet_ex3 : forall A B C,
Bet A B C ->
exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.
induction (eq_dec_points A B).
induction (eq_dec_points B C).
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
subst C.
subst A.
assumption.
subst A.
subst C.
assumption.
assumption.
unfold Col.
left.
subst A.
subst C.
assumption.
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.
apply between_symmetry in H.
apply H1.
eapply between_egality.
apply H2.
apply H.
intro.
subst D.
subst A.
apply between_identity in H2.
apply H3.
subst B.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
apply H2.
assumption.
induction (eq_dec_points B C).
subst C.
cut(exists D : Tpoint, A <> D /\ B <> D /\ Col A B D).
intro.
ex_and H1 D.
exists D.
repeat split.
assumption.
assumption.
assumption.
assumption.
apply diff_col_ex.
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.
assert (B = C).
eapply between_egality.
apply H2.
apply between_symmetry.
assumption.
apply H1.
assumption.
intro.
subst D.
apply between_identity in H2.
subst C.
apply H1.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
assumption.
assumption.
Qed.
Lemma diff_col_ex3 : forall A B C,
Col A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.
assert(cas1 := diff_bet_ex3 A B C).
assert(cas2 := diff_bet_ex3 B C A).
assert(cas3 := diff_bet_ex3 C A B).
unfold Col in H.
induction H.
apply (diff_bet_ex3 A B C).
assumption.
induction H.
assert (HH:=H).
induction (eq_dec_points B C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
apply cas2 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H0.
assumption.
unfold Col.
left.
assumption.
induction (eq_dec_points A C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
assert (HH:=H).
apply cas3 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_5.
eapply col_transitivity_1.
apply H0.
apply col_permutation_4.
assumption.
unfold Col.
right;right.
apply between_symmetry.
assumption.
Qed.
Lemma mid_preserve_col : forall A B C M A' B' C',
Col A B C ->
is_midpoint M A A' ->
is_midpoint M B B' ->
is_midpoint M C C' ->
Col A' B' C'.
Proof.
intros.
induction H.
assert (Bet A' B' C').
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
unfold Col.
left.
assumption.
induction H.
assert (Bet B' C' A').
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
unfold Col.
right; left.
assumption.
assert (Bet C' A' B').
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
unfold Col.
right; right.
assumption.
Qed.
Lemma per_mid_per : forall A B X Y M,
A <> B -> Per X A B -> is_midpoint M A B -> is_midpoint M X Y ->
Cong A X B Y /\ Per Y B A.
Proof.
intros.
assert (Cong A X B Y).
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.
split.
assumption.
unfold Per in H0.
ex_and H0 B'.
double A B A'.
assert (Cong B X A Y).
eapply l7_13.
apply H1.
apply l7_2.
assumption.
assert (OFSC B A B' X A B A' Y).
unfold OFSC.
repeat split.
apply mid_bet.
assumption.
apply mid_bet.
assumption.
apply cong_pseudo_reflexivity.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H8.
apply cong_left_commutativity.
assumption.
assumption.
assumption.
unfold Per.
exists A'.
split.
assumption.
assert (Cong B' X A' Y).
eapply five_segments_with_def.
apply H7.
intro.
apply H.
subst B.
reflexivity.
eapply cong_transitivity.
apply cong_commutativity.
apply cong_symmetry.
apply H6.
eapply cong_transitivity.
apply H4.
apply cong_commutativity.
assumption.
Qed.
Lemma perp_in_perp : forall A B C D X,
Perp_in X A B C D -> Perp X B C D \/ Perp A X C D.
Proof.
intros.
induction (eq_dec_points X A).
subst X.
left.
unfold Perp.
exists A.
assumption.
right.
unfold Perp.
exists X.
unfold Perp_in in *.
spliter.
repeat split.
intro.
apply H0.
subst X.
reflexivity.
assumption.
apply col_trivial_3.
assumption.
intros.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H7.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
assumption.
Qed.
Lemma perp_col_2 : forall A B C D X Y,
Perp A B C D -> X <> Y -> Col A B X -> Col A B Y -> Perp X Y C D.
Proof.
intros.
unfold Perp in *.
ex_elim H M.
exists M.
unfold Perp_in in *.
spliter.
repeat split.
assumption.
assumption.
eapply col_col.
apply H.
Col.
assumption.
assumption.
assumption.
intros.
apply H6.
eapply col_col.
apply H0.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
assumption.
Qed.
Lemma sym_preserve_diff : forall A B M A' B',
A <> B -> is_midpoint M A A' -> is_midpoint M B B' -> A'<> B'.
Proof.
intros.
intro.
subst B'.
assert (A = B).
eapply l7_9.
apply H0.
assumption.
contradiction.
Qed.
Lemma perp_col2 : forall P Q R S A B,
Perp P Q A B -> Col P Q R -> Col P Q S -> R <> S ->
Perp R S A B.
Proof.
intros.
induction (eq_dec_points P R).
induction (eq_dec_points P S).
subst R.
subst S.
absurde.
subst P.
eapply perp_col.
2:apply H.
assumption.
assumption.
induction (eq_dec_points Q R).
induction (eq_dec_points Q S).
subst R.
subst Q.
absurde.
subst Q.
eapply perp_col.
2:apply perp_left_comm.
2 :apply H.
assumption.
apply col_permutation_4.
assumption.
eapply perp_col.
2: apply perp_left_comm.
2: eapply perp_col.
3:apply H.
assumption.
assumption.
assumption.
eapply col_col.
apply perp_distinct in H.
spliter.
apply H.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma l9_4_1_aux : forall P Q A C R S M,
le S C R A ->
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> is_midpoint M R S ->
(forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
Proof.
intros.
induction (eq_dec_points R S).
subst S.
apply l7_3 in H5.
subst R.
unfold two_sides in H0.
spliter.
ex_and H8 T.
assert (T=M).
eapply inter_unicity.
apply col_permutation_1.
apply H8.
unfold Col.
right; left.
apply H9.
apply col_permutation_1.
assumption.
induction (eq_dec_points M P).
assert(Q <> M).
intro.
subst P.
subst Q.
apply perp_distinct in H2.
apply H0.
reflexivity.
assert(M <> Q).
intro.
apply H11.
subst Q.
reflexivity.
assert (Perp Q M A M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H2.
apply col_permutation_3.
assumption.
apply perp_left_comm in H13.
eapply perp_id in H13.
apply perp_in_comm in H13.
eapply perp_in_per in H13.
assert (Perp Q M C M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_3.
assumption.
apply perp_left_comm in H14.
eapply perp_id in H14.
apply perp_in_comm in H14.
eapply perp_in_per in H14.
eapply per_per_col.
apply l8_2.
apply H14.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
assert (Perp P M A M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H2.
apply col_permutation_1.
assumption.
apply perp_left_comm in H11.
eapply perp_id in H11.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
assert (Perp P M C M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H4.
apply col_permutation_1.
assumption.
apply perp_left_comm in H12.
eapply perp_id in H12.
apply perp_in_comm in H12.
eapply perp_in_per in H12.
eapply per_per_col.
apply l8_2.
apply H12.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
intro.
apply H7.
apply col_permutation_4.
assumption.
intro.
subst C.
apply between_identity in H9.
subst A.
apply H5.
assumption.
subst T.
split.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
intro.
subst C'.
apply l7_2 in H6.
eapply (midpoint_id _ _ M) in H6.
apply H10.
apply sym_equal.
apply H6.
apply l7_3_2.
induction H12.
assert (Bet U M C).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
unfold is_midpoint in H13.
spliter.
eapply l5_2.
apply H10.
assumption.
apply mid_bet.
assumption.
assert (Bet U M C).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply l5_2.
apply H10.
assumption.
unfold is_midpoint in H6.
spliter.
assumption.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst U.
eapply is_midpoint_id in H6.
subst C'.
apply H11.
reflexivity.
intro.
subst A.
apply perp_distinct in H2.
spliter.
apply H13.
reflexivity.
unfold is_midpoint in H6.
spliter.
assert (Bet A M C').
induction H12.
eapply outer_transitivity_between.
apply H9.
assumption.
intro.
apply H10.
subst C.
reflexivity.
eapply between_inner_transitivity.
apply H9.
assumption.
eapply l5_2.
apply H11.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
unfold le in H.
ex_and H D.
assert (C <> S).
intro.
subst S.
apply perp_distinct in H4.
spliter.
absurde.
assert (R <> D).
intro.
subst D.
apply cong_identity in H8.
apply H9.
subst S.
reflexivity.
assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert(exists M, is_midpoint M S R /\ is_midpoint M C D).
unfold two_sides in H0.
spliter.
ex_and H14 T.
eapply (l8_24 S R C A D T).
apply perp_sym.
apply perp_left_comm.
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
apply perp_right_comm.
apply perp_sym.
assumption.
eapply col_col.
apply H0.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.
ex_and H12 M'.
apply l7_2 in H12.
assert (M = M').
eapply l7_17.
apply H5.
apply H12.
subst M'.
split.
intro.
unfold out in H14.
spliter.
unfold out.
repeat split.
assumption.
eapply sym_preserve_diff.
2:apply H6.
apply H14.
assumption.
induction H16.
Focus 2.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
eapply between_exchange4.
apply H.
apply H16.
assert(Bet R U D \/ Bet R D U).
eapply l5_3.
apply H16.
assumption.
induction H17.
right.
eapply l7_15.
apply H5.
apply H6.
apply l7_2.
apply H13.
assumption.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
assumption.
unfold out.
intros.
spliter.
repeat split.
eapply sym_preserve_diff.
apply H15.
apply l7_2.
apply H6.
apply l7_2.
assumption.
intro.
subst R.
apply perp_distinct in H11.
spliter.
absurde.
induction H16.
eapply l5_1.
apply H10.
eapply l7_15.
apply l7_2.
apply H12.
apply H13.
apply l7_2.
apply H6.
assumption.
assumption.
left.
eapply between_exchange4.
eapply l7_15.
apply l7_2.
apply H12.
apply l7_2.
apply H6.
apply H13.
assumption.
assumption.
Qed.
Lemma per_col_eq : forall A B C, Per A B C -> Col A B C -> B <> C -> A = B.
Proof.
intros.
unfold Per in H.
ex_and H C'.
assert (Col A C C').
eapply col_col.
apply H1.
apply col_permutation_1.
assumption.
apply col_trivial_2.
unfold Col.
right; right.
apply between_symmetry.
apply mid_bet.
assumption.
assert (C = C' \/ is_midpoint A C C').
eapply l7_20.
apply col_permutation_4.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H.
contradiction.
eapply l7_17.
apply H4.
assumption.
Qed.
Lemma l9_4_1 : forall P Q A C R S M, two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> is_midpoint M R S -> (forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
intros.
assert (le S C R A \/ le R A S C).
apply le_cases.
induction H6.
apply (l9_4_1_aux P Q A C R S M); assumption.
assert((out R A U <-> out S C' C) -> (out R U A <-> out S C C')).
intro.
induction H7.
split.
intro.
eapply l6_6.
apply H7.
apply l6_6.
assumption.
intro.
apply l6_6.
apply H8.
apply l6_6.
assumption.
apply H7.
assert((out S C' C <-> out R A U) -> (out R A U <-> out S C' C)).
intro.
induction H8.
split.
intro.
apply H9.
assumption.
intro.
apply H8.
assumption.
apply H8.
eapply (l9_4_1_aux).
assumption.
apply l9_2.
apply H.
assumption.
assumption.
assumption.
assumption.
apply l7_2.
apply H4.
apply l7_2.
assumption.
Qed.
Lemma mid_two_sides : forall A B M X Y, A <> B -> is_midpoint M A B -> ~Col A B X -> is_midpoint M X Y -> two_sides A B X Y.
intros.
unfold two_sides.
repeat split.
assumption.
intro.
apply col_permutation_1 in H3.
contradiction.
intro.
apply H1.
unfold is_midpoint in *.
spliter.
assert (Col A M Y).
eapply col_transitivity_1.
apply H.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
assert (Col B M Y).
eapply col_transitivity_1.
intro.
apply H.
apply sym_equal.
apply H7.
unfold Col.
right; left.
assumption.
apply col_permutation_3.
assumption.
assert (Y <> M).
intro.
subst M.
apply cong_identity in H4.
subst Y.
apply H1.
apply col_permutation_1.
assumption.
assert (Col Y A X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
assert (Col Y B X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
assert (X <> Y).
intro.
subst Y.
apply between_identity in H2.
contradiction.
apply col_permutation_1.
eapply col_transitivity_1.
apply H11.
apply col_permutation_2.
assumption.
apply col_permutation_2.
assumption.
exists M.
unfold is_midpoint in *.
spliter.
split.
unfold Col.
right; right.
apply between_symmetry.
assumption.
assumption.
Qed.
Lemma col_preserves_two_sides : forall A B C D X Y, A <> B -> C <> D -> Col A B C -> Col A B D -> two_sides A B X Y -> two_sides C D X Y.
intros.
unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H4.
apply col_permutation_1.
eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
intro.
apply H5.
apply col_permutation_1.
eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
ex_and H6 T.
exists T.
split.
eapply col_col.
apply H3.
apply col_permutation_1.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma out_out_two_sides : forall A B X Y U V I, A <> B -> two_sides A B X Y -> Col I A B -> Col I X Y
-> out I X U -> out I Y V -> two_sides A B U V.
intros.
unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H5.
unfold out in H3.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
intro.
apply H6.
unfold out in H4.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
ex_and H7 T.
assert (I = T).
eapply inter_unicity.
apply col_permutation_1.
apply H1.
apply col_permutation_1.
apply H2.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
intro.
subst Y.
apply between_identity in H8.
subst X.
apply H5.
assumption.
subst I.
exists T.
split.
assumption.
unfold out in *.
spliter.
induction H12; induction H10.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
auto.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply between_inner_transitivity.
apply H13.
assumption.
assert (Bet U T Y).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
intro.
subst Y.
apply H6.
assumption.
assert (Bet V T X).
eapply between_exchange3.
apply between_symmetry.
apply H10.
apply between_symmetry.
assumption.
eapply between_exchange3.
apply between_symmetry.
apply H12.
apply between_symmetry.
assumption.
Qed.
Lemma out_out_two_sides1 : forall P Q A C M U V,
two_sides P Q A C -> Col M P Q -> Perp P Q A M ->
Perp P Q C M -> out M U A -> out M V C -> two_sides P Q U V.
intros.
eapply out_out_two_sides.
unfold two_sides in H.
spliter.
assumption.
apply H.
apply H0.
unfold two_sides in H.
spliter.
ex_and H7 T.
induction(eq_dec_points M P).
assert(M <> Q).
intro.
subst P.
subst Q.
absurde.
subst P.
apply perp_id in H1.
apply perp_in_comm in H1.
eapply perp_in_per in H1.
apply perp_id in H2.
apply perp_in_comm in H2.
eapply perp_in_per in H2.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H1.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
assert (Perp M P A M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H1.
apply col_permutation_1.
assumption.
assert(Perp M P C M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H2.
apply col_permutation_1.
assumption.
apply perp_id in H10.
apply perp_id in H11.
apply perp_in_comm in H10.
eapply perp_in_per in H10.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H10.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
apply l6_6.
assumption.
apply l6_6.
assumption.
Qed.
Lemma mid_preserves_col : forall A B C A' B' C' M, Col A B C -> is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
-> Col A' B' C'.
intros.
unfold Col in *.
induction H.
left.
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
induction H.
right; left.
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
right; right.
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
Qed.
Lemma l9_4_2_aux : forall P Q A C R S U V, le S C R A ->
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.
induction (eq_dec_points R S).
subst S.
eapply out_out_two_sides1.
apply H0.
apply H1.
assumption.
assumption.
assumption.
assumption.
assert(P <> Q).
apply perp_distinct in H4.
spliter.
assumption.
assert (two_sides R S A C).
eapply (col_preserves_two_sides P Q).
assumption.
apply H7.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
eapply (col_preserves_two_sides R S).
assumption.
assumption.
eapply col_permutation_1.
eapply col2.
apply H8.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.
assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert (Perp R S C S).
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert (HH9:=H9).
unfold two_sides in HH9.
spliter.
ex_and H15 T.
unfold le in H.
ex_and H C'.
assert (exists M, is_midpoint M S R /\ is_midpoint M C C').
eapply (l8_24 S R C A C' T).
apply perp_sym.
apply perp_left_comm.
assumption.
apply
perp_sym.
apply perp_left_comm.
assumption.
apply col_permutation_3.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.
ex_and H18 M.
double U M U'.
assert (R <> U).
intro.
subst U.
unfold out in H5.
spliter.
absurde.
assert (two_sides R S U U').
eapply mid_two_sides.
assumption.
apply l7_2.
apply H18.
intro.
apply H13.
eapply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply col_permutation_5.
assumption.
induction H5.
spliter.
induction H24.
unfold Col.
left.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
assumption.
apply l9_2.
eapply l9_3.
apply l9_2.
apply H22.
unfold Col.
right; right.
apply mid_bet.
apply H18.
apply l7_2.
assumption.
apply col_trivial_3.
assert (forall X Y, is_midpoint M X Y -> (out R X A <-> out S C Y)).
eapply l9_4_1.
apply H9.
apply col_trivial_1.
assumption.
apply col_trivial_3.
assumption.
apply l7_2.
assumption.
assert (out R U A <-> out S C U').
eapply H23.
assumption.
destruct H24.
eapply l6_7.
apply l6_6.
apply H24.
assumption.
apply l6_6.
assumption.
Qed.
Lemma l9_4_2 : forall P Q A C R S U V,
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.
assert( le S C R A \/ le R A S C).
apply le_cases.
induction H6.
eapply l9_4_2_aux.
apply H6.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
apply l9_2.
eapply l9_4_2_aux.
apply H6.
apply l9_2.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma l9_5 : forall P Q A C R B,
two_sides P Q A C -> Col R P Q -> out R A B -> two_sides P Q B C.
intros.
assert (P <> Q).
unfold two_sides in H.
spliter.
assumption.
assert(exists A0, Col P Q A0 /\ Perp P Q A A0).
eapply l8_18_existence.
intro.
unfold two_sides in H.
spliter.
apply H4.
apply col_permutation_2.
assumption.
assert(exists C0, Col P Q C0 /\ Perp P Q C C0).
eapply l8_18_existence.
unfold two_sides in H.
spliter.
intro.
apply H5.
apply col_permutation_2.
assumption.
assert(exists B0, Col P Q B0 /\ Perp P Q B B0).
eapply l8_18_existence.
assert (HH1:=H1).
unfold out in HH1.
unfold two_sides in H.
spliter.
intro.
assert (Col P B R).
eapply col2.
apply H.
assumption.
apply col_permutation_1.
assumption.
assert (R <> B).
intro.
subst B.
absurde.
assert(Col R P A ).
eapply col2.
apply H13.
eapply col_permutation_3.
assumption.
apply col_permutation_5.
apply out_col.
assumption.
apply H8.
eapply col_permutation_2.
eapply col2.
apply H.
apply col_trivial_2.
eapply colx.
assumption.
3:apply col_permutation_1.
3:apply H0.
3: apply H11.
assumption.
assumption.
apply col_permutation_5.
apply out_col.
assumption.
ex_and H3 A'.
ex_and H4 C'.
ex_and H5 B'.
assert (exists M, is_midpoint M A' C').
apply midpoint_existence.
ex_and H9 M.
double A M D.
assert (out C' D C <-> out A' A A).
eapply l9_4_1.
apply l9_2.
apply H.
apply col_permutation_2.
assumption.
assumption.
apply col_permutation_2.
assumption.
assumption.
apply l7_2.
apply H10.
apply l7_2.
assumption.
destruct H11.
assert (out C' D C).
apply H12.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.
assert (two_sides P Q A D).
eapply l9_4_2.
apply H.
apply col_permutation_2.
apply H3.
assumption.
apply col_permutation_2.
apply H4.
apply H7.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.
assumption.
assert (two_sides P Q B D).
eapply l9_3.
apply H14.
2:apply H9.
2: apply H0.2:assumption.
induction (eq_dec_points A' C').
subst C'.
apply l7_3 in H10.
subst A'.
apply col_permutation_2.
assumption.
eapply col_permutation_2.
eapply colx.
assumption.
apply H15.
intro.
subst C'.
eapply l7_2 in H10.
eapply midpoint_id in H10.
apply H15.
apply sym_equal.
apply H10.
apply l7_3_2.
assumption.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
try assumption.
eapply l9_4_2.
apply H15.
2: apply H8.
apply col_permutation_2.
assumption.
apply col_permutation_2.
apply H4.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst D.
unfold out in H13.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H7.
apply col_permutation_5.
apply out_col.
assumption.
eapply out_trivial.
intro.
subst B.
apply perp_distinct in H8.
spliter.
absurde.
apply l6_6.
assumption.
Qed.
Lemma outer_pasch : forall A B C P Q,
Bet A C P -> Bet B Q C -> exists X, Bet A X B /\ Bet P Q X.
Proof.
intros.
induction(classic (Col P Q C)).
induction(classic (Bet P Q C)).
exists A.
split.
apply between_symmetry.
apply between_trivial.
eapply between_exchange4.
apply H2.
apply between_symmetry.
assumption.
assert (out Q P C).
eapply l6_4_2.
split;trivial.
exists B.
split.
apply between_trivial.
unfold out in H3.
spliter.
induction H5.
eapply between_exchange3.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
eapply outer_transitivity_between2.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
assumption.
induction (eq_dec_points B Q).
subst Q.
exists B.
split; apply between_trivial.
assert (A <> P).
intro.
subst P.
apply between_identity in H.
subst C.
apply False_ind.
apply H1.
apply col_trivial_3.
assert (P <> Q).
intro.
subst Q.
apply H1.
apply col_trivial_1.
assert (P <> B).
intro.
subst P.
apply H1.
unfold Col.
left.
assumption.
assert(two_sides P Q C B).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
apply col_permutation_1.
assumption.
intro.
apply H1.
assert (Col B P C ).
eapply col2.
apply H2.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
eapply col2.
apply H5.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
exists Q.
split.
apply col_trivial_3.
apply between_symmetry.
assumption.
assert (two_sides P Q A B).
eapply l9_5.
apply H6.
apply col_trivial_1.
unfold out.
repeat split.
intro.
subst P.
apply H1.
apply col_trivial_3.
assumption.
left.
apply between_symmetry.
assumption.
unfold two_sides in H7.
spliter.
ex_and H10 X.
exists X.
split.
assumption.
assert (exists T, Bet X T P /\ Bet C T B).
eapply inner_pasch.
apply between_symmetry.
apply H11.
apply between_symmetry.
assumption.
ex_and H12 T.
assert (T = Q).
eapply inter_unicity.
unfold Col.
right; left.
apply H12.
unfold Col.
right; left.
apply H13.
apply col_permutation_4.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H9.
eapply col_permutation_2.
eapply col2.
2: apply col_permutation_4.
2:apply H10.
intro.
subst X.
apply H8.
eapply colx.
assumption.
3: unfold Col.
3:right; left.
3:apply between_symmetry.
3:apply H.
3: unfold Col.
3: left.
3: apply H11.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H12.
subst P.
apply H1.
apply col_trivial_3.
intro.
subst Q.
unfold two_sides in H6.
spliter.
apply H15.
apply col_trivial_3.
unfold Col.
right; left.
assumption.
apply col_permutation_5.
assumption.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H0.
subst Q.
apply H1.
apply col_trivial_2.
subst T.
apply between_symmetry.
assumption.
Qed.
Definition one_side := fun P Q A B =>
exists C, two_sides P Q A C /\ two_sides P Q B C.
Lemma l9_8_1 : forall P Q A B C, two_sides P Q A C -> two_sides P Q B C -> one_side P Q A B.
intros.
unfold one_side.
exists C.
split; assumption.
Qed.
Lemma not_two_sides_id : forall A P Q, ~ two_sides P Q A A.
intros.
intro.
unfold two_sides in H.
spliter.
ex_and H2 T.
apply between_identity in H3.
subst T.
apply H0.
apply H2.
Qed.
Lemma l9_8_2 : forall P Q A B C, two_sides P Q A C -> (one_side P Q A B -> two_sides P Q B C).
intros.
unfold one_side in H0.
ex_and H0 D.
assert (HH:= H).
assert (HH0:=H0).
assert (HH1:=H1).
unfold two_sides in HH.
unfold two_sides in HH0.
unfold two_sides in HH1.
spliter.
ex_and H13 T.
ex_and H9 X.
ex_and H5 Y.
assert (exists M , Bet Y M A /\ Bet X M B).
eapply inner_pasch.
apply H16.
apply H15.
ex_and H17 M.
assert (A <> D).
intro.
subst D.
apply not_two_sides_id in H0.
assumption.
assert (B <> D).
intro.
subst D.
apply not_two_sides_id in H1.
assumption.
induction (classic(Col A B D)).
induction (eq_dec_points M Y).
subst M.
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
apply col_permutation_3.
assumption.
apply bet_col in H16.
Col.
intro.
Col.
auto.
subst Y.
eapply l9_5.
apply H.
apply H9.
unfold out.
repeat split.
intro.
subst X.
apply H11.
assumption.
intro.
subst X.
apply H3.
assumption.
unfold Col in H21.
induction H21.
right.
eapply between_exchange3.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
induction H21.
assert (Bet D B A \/ Bet D A B).
eapply (l5_1 _ X).
intro.
subst X.
apply H4.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
induction H22.
assert (D = B).
eapply between_egality.
apply H22.
apply H21.
subst D.
absurde.
assert (D = A).
eapply between_egality.
apply H22.
apply between_symmetry.
assumption.
subst D.
absurde.
eapply (l5_2 D).
intro.
subst X.
apply H8.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
induction (eq_dec_points M X).
subst M.
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
Col.
apply bet_col in H16.
Col.
intro.
apply H4.
apply col_permutation_4.
assumption.
auto.
subst Y.
absurde.
eapply (l9_5 _ _ M _ X).
eapply l9_5.
apply H.
apply H5.
unfold out.
repeat split.
intro.
subst Y.
apply between_identity in H17.
subst M.
absurde.
assumption.
right.
assumption.
assumption.
unfold out.
assert (out Y M A).
unfold out.
repeat split.
assumption.
intro.
subst Y.
apply H11.
assumption.
left.
assumption.
repeat split.
assumption.
intro.
subst X.
apply between_identity in H18.
subst M.
absurde.
left.
apply H18.
eapply (l9_5 _ _ M).
eapply l9_5.
apply H.
apply H5.
unfold out.
repeat split.
intro.
subst Y.
apply H7.
assumption.
intro.
subst Y.
assert(Col B D X).
eapply (col2 _ M).
intro.
subst M.
apply H3.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ X).
intro.
subst X.
apply H4.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
right.
assumption.
apply H9.
unfold out.
repeat split.
intro.
subst X.
assert (Col A D Y).
eapply (col2 _ M).
intro.
subst M.
apply H7.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ Y).
intro.
subst Y.
apply H4.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
intro.
subst X.
apply H3.
assumption.
left.
assumption.
Qed.
Lemma l9_9 : forall P Q A B, two_sides P Q A B -> ~ one_side P Q A B.
intros.
intro.
assert(L:=l9_8_2).
apply (L P Q A B B )in H.
apply not_two_sides_id in H.
assumption.
assumption.
Qed.
Lemma l9_9_bis : forall P Q A B, one_side P Q A B -> ~ two_sides P Q A B.
intros.
intro.
unfold one_side in H.
ex_and H C.
assert (one_side P Q A B).
eapply l9_8_1.
apply H.
assumption.
assert (~ one_side P Q A B).
apply l9_9.
assumption.
contradiction.
Qed.
Lemma l9_10 : forall P Q A,
P<>Q -> ~ Col A P Q -> exists C, two_sides P Q A C.
Proof.
intros.
double A P A'.
exists A'.
unfold two_sides.
repeat split.
assumption.
assumption.
intro.
apply H0.
eapply col_permutation_2.
eapply (col2 _ A').
intro.
subst A'.
apply l7_2 in H1.
eapply is_midpoint_id in H1.
subst A.
apply H0.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
Qed.
Lemma one_side_reflexivity : forall P Q A,
~ Col A P Q -> one_side P Q A A.
Proof.
intros.
unfold one_side.
double A P C.
exists C.
assert (two_sides P Q A C).
repeat split.
intro.
subst Q.
apply H.
apply col_trivial_2.
assumption.
intro.
apply H.
apply col_permutation_2.
eapply (col2 _ C).
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst A.
apply H.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
split; assumption.
Qed.
Lemma one_side_symmetry : forall P Q A B,
one_side P Q A B -> one_side P Q B A.
Proof.
unfold one_side.
intros.
ex_and H C.
exists C.
split; assumption.
Qed.
Lemma one_side_transitivity : forall P Q A B C,
one_side P Q A B -> one_side P Q B C -> one_side P Q A C.
Proof.
intros.
unfold one_side in *.
ex_and H X.
ex_and H0 Y.
exists X.
split.
assumption.
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H2.
eapply l9_8_1.
apply l9_2.
apply H0.
apply l9_2.
assumption.
Qed.
End T9.
Section T9.
Context `{MT: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.
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.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Ltac double A B A' :=
assert (mp:= mdp A B);
elim mp; intros A' ; intro; clear mp.
Definition two_sides := fun A B P Q =>
A<>B /\ ~ Col P A B /\ ~ Col Q A B /\ exists T, Col T A B /\ Bet P T Q.
Lemma l9_2 : forall A B P Q, two_sides A B P Q -> two_sides A B Q P.
unfold two_sides.
intros.
spliter.
repeat split;try assumption.
ex_and H2 T.
exists T.
split;
Between.
Qed.
Lemma inter_unicity : forall A B X Y M N, Col A B M-> Col X Y M -> Col A B N -> Col X Y N ->
~ Col A X B -> X <> Y -> M = N.
intros.
eapply l6_21.
3:apply H.
4: apply H0.
intro.
apply H3.
apply col_permutation_5.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma col2 : forall A B X Y, A <> B -> Col A B X -> Col A B Y -> Col A X Y.
intros.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
Qed.
Lemma colx : forall A B M N X, A <> B -> N <> M -> X <> M -> Col A B M -> Col A B N -> Col M N X -> Col A B X.
intros.
assert (Col A M N).
eapply col2.
apply H.
assumption.
assumption.
assert(Col B M N).
eapply (col2 B A).
auto.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
assert (Col M A X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.
assert(Col M B X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.
apply col_permutation_2 in H6.
apply col_permutation_2 in H7.
apply col_permutation_1.
eapply (col2).
apply H1.
assumption.
apply col_permutation_2.
assumption.
Qed.
Lemma l9_3 : forall P Q A C M R B,
two_sides P Q A C -> Col M P Q ->
is_midpoint M A C -> Col R P Q ->
out R A B -> two_sides P Q B C.
Proof.
intros.
unfold two_sides in *.
spliter.
ex_and H6 T.
assert (A <> C).
intro.
subst C.
eapply l7_3 in H1.
subst M.
apply H4.
assumption.
assert (T = M).
eapply inter_unicity.
apply col_permutation_1.
apply H6.
unfold Col.
right; left.
apply H7.
apply col_permutation_1.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
auto.
subst T.
repeat split.
assumption.
2:assumption.
induction(eq_dec_points C M).
subst M.
intro.
apply H5.
assumption.
intro.
clear H0.
assert (B <> R).
intro.
subst B.
unfold out in H3.
spliter.
absurde.
assert (Col P R B).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col P R A).
induction (eq_dec_points P B).
subst B.
unfold out in H3.
spliter.
induction H13.
unfold Col.
right; left.
apply H13.
unfold Col.
right; right.
apply between_symmetry.
assumption.
apply col_permutation_2.
eapply col_transitivity_2.
apply H0.
unfold Col.
unfold out in H3.
spliter.
induction H14.
right; left.
assumption.
right; right.
apply between_symmetry.
assumption.
apply col_permutation_3.
assumption.
induction (eq_dec_points P R).
subst R.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ B).
unfold out in H3.
spliter.
auto.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H14.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
assert (Col P B A ).
eapply col_transitivity_1.
apply H13.
assumption.
assumption.
induction (eq_dec_points P B).
subst B.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ R).
apply H0.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H16.
right; left.
assumption.
right;right.
apply between_symmetry.
assumption.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H15.
apply col_permutation_4.
assumption.
assumption.
induction H3.
spliter.
induction H10.
Focus 2.
assert (exists X, Bet B X C /\ Bet M X R).
eapply inner_pasch.
apply H10.
apply between_symmetry.
assumption.
ex_and H11 X.
exists X.
induction (eq_dec_points M R).
subst R.
apply between_identity in H12.
subst X.
split; assumption.
induction (eq_dec_points R X).
subst X.
split; assumption.
split.
induction (eq_dec_points X M).
subst X.
assumption.
assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col X P Q).
apply col_permutation_2.
eapply colx.
assumption.
apply H13.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
assumption.
assumption.
assumption.
double B M B'.
double R M R'.
assert (Bet B' C R').
eapply l7_15.
apply H11.
apply H1.
apply H12.
apply between_symmetry.
assumption.
assert (exists X, Bet M X R' /\ Bet C X B).
eapply inner_pasch.
apply mid_bet.
apply H11.
apply between_symmetry.
assumption.
ex_and H14 X.
exists X.
split.
assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assert (Col Q M R).
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.
induction (eq_dec_points M X).
subst X.
assumption.
induction (eq_dec_points M R').
subst R'.
apply between_identity in H14.
subst X.
absurde.
assert (M <> R).
intro.
subst R.
eapply (midpoint_id) in H12.
apply H19.
apply H12.
apply l7_3_2.
apply col_permutation_2.
eapply (colx _ _ M R).
assumption.
auto.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
eapply (col_transitivity_1).
apply H20.
apply col_trivial_2.
eapply col_transitivity_1.
apply H19.
unfold Col.
right; right.
apply mid_bet.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
Qed.
Definition is_symmetric (A A' C : Tpoint) := is_midpoint C A A'.
Lemma sym_sym : forall A C A', is_symmetric A A' C -> is_symmetric A' A C.
unfold is_symmetric.
intros.
apply l7_2.
assumption.
Qed.
Lemma distinct : forall P Q R : Tpoint, P <> Q -> (R <> P \/ R <> Q).
Proof.
intros.
assert (~ (R = P /\ R = Q) -> (R <> P \/ R <> Q)).
intro.
induction (eq_dec_points P R).
subst R.
right.
intro.
apply H0.
split.
reflexivity.
assumption.
left.
intro.
apply H1.
subst R.
reflexivity.
apply H0.
intro.
spliter.
subst P.
subst Q.
apply H.
reflexivity.
Qed.
Lemma diff_col_ex : forall A B, exists C, A <> C /\ B <> C /\ Col A B C.
intros.
assert (exists C, Bet A B C /\ B <> C).
apply point_construction_different.
ex_and H C.
exists C.
split.
intro.
induction (eq_dec_points A B).
subst B.
subst C.
apply H0.
reflexivity.
subst C.
apply between_identity in H.
subst B.
apply H0.
reflexivity.
split.
assumption.
unfold Col.
left.
assumption.
Qed.
Lemma diff_bet_ex3 : forall A B C,
Bet A B C ->
exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.
induction (eq_dec_points A B).
induction (eq_dec_points B C).
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
subst C.
subst A.
assumption.
subst A.
subst C.
assumption.
assumption.
unfold Col.
left.
subst A.
subst C.
assumption.
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.
apply between_symmetry in H.
apply H1.
eapply between_egality.
apply H2.
apply H.
intro.
subst D.
subst A.
apply between_identity in H2.
apply H3.
subst B.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
apply H2.
assumption.
induction (eq_dec_points B C).
subst C.
cut(exists D : Tpoint, A <> D /\ B <> D /\ Col A B D).
intro.
ex_and H1 D.
exists D.
repeat split.
assumption.
assumption.
assumption.
assumption.
apply diff_col_ex.
assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.
assert (B = C).
eapply between_egality.
apply H2.
apply between_symmetry.
assumption.
apply H1.
assumption.
intro.
subst D.
apply between_identity in H2.
subst C.
apply H1.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
assumption.
assumption.
Qed.
Lemma diff_col_ex3 : forall A B C,
Col A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.
assert(cas1 := diff_bet_ex3 A B C).
assert(cas2 := diff_bet_ex3 B C A).
assert(cas3 := diff_bet_ex3 C A B).
unfold Col in H.
induction H.
apply (diff_bet_ex3 A B C).
assumption.
induction H.
assert (HH:=H).
induction (eq_dec_points B C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
apply cas2 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H0.
assumption.
unfold Col.
left.
assumption.
induction (eq_dec_points A C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
assert (HH:=H).
apply cas3 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_5.
eapply col_transitivity_1.
apply H0.
apply col_permutation_4.
assumption.
unfold Col.
right;right.
apply between_symmetry.
assumption.
Qed.
Lemma mid_preserve_col : forall A B C M A' B' C',
Col A B C ->
is_midpoint M A A' ->
is_midpoint M B B' ->
is_midpoint M C C' ->
Col A' B' C'.
Proof.
intros.
induction H.
assert (Bet A' B' C').
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
unfold Col.
left.
assumption.
induction H.
assert (Bet B' C' A').
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
unfold Col.
right; left.
assumption.
assert (Bet C' A' B').
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
unfold Col.
right; right.
assumption.
Qed.
Lemma per_mid_per : forall A B X Y M,
A <> B -> Per X A B -> is_midpoint M A B -> is_midpoint M X Y ->
Cong A X B Y /\ Per Y B A.
Proof.
intros.
assert (Cong A X B Y).
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.
split.
assumption.
unfold Per in H0.
ex_and H0 B'.
double A B A'.
assert (Cong B X A Y).
eapply l7_13.
apply H1.
apply l7_2.
assumption.
assert (OFSC B A B' X A B A' Y).
unfold OFSC.
repeat split.
apply mid_bet.
assumption.
apply mid_bet.
assumption.
apply cong_pseudo_reflexivity.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H8.
apply cong_left_commutativity.
assumption.
assumption.
assumption.
unfold Per.
exists A'.
split.
assumption.
assert (Cong B' X A' Y).
eapply five_segments_with_def.
apply H7.
intro.
apply H.
subst B.
reflexivity.
eapply cong_transitivity.
apply cong_commutativity.
apply cong_symmetry.
apply H6.
eapply cong_transitivity.
apply H4.
apply cong_commutativity.
assumption.
Qed.
Lemma perp_in_perp : forall A B C D X,
Perp_in X A B C D -> Perp X B C D \/ Perp A X C D.
Proof.
intros.
induction (eq_dec_points X A).
subst X.
left.
unfold Perp.
exists A.
assumption.
right.
unfold Perp.
exists X.
unfold Perp_in in *.
spliter.
repeat split.
intro.
apply H0.
subst X.
reflexivity.
assumption.
apply col_trivial_3.
assumption.
intros.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H7.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
assumption.
Qed.
Lemma perp_col_2 : forall A B C D X Y,
Perp A B C D -> X <> Y -> Col A B X -> Col A B Y -> Perp X Y C D.
Proof.
intros.
unfold Perp in *.
ex_elim H M.
exists M.
unfold Perp_in in *.
spliter.
repeat split.
assumption.
assumption.
eapply col_col.
apply H.
Col.
assumption.
assumption.
assumption.
intros.
apply H6.
eapply col_col.
apply H0.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
assumption.
Qed.
Lemma sym_preserve_diff : forall A B M A' B',
A <> B -> is_midpoint M A A' -> is_midpoint M B B' -> A'<> B'.
Proof.
intros.
intro.
subst B'.
assert (A = B).
eapply l7_9.
apply H0.
assumption.
contradiction.
Qed.
Lemma perp_col2 : forall P Q R S A B,
Perp P Q A B -> Col P Q R -> Col P Q S -> R <> S ->
Perp R S A B.
Proof.
intros.
induction (eq_dec_points P R).
induction (eq_dec_points P S).
subst R.
subst S.
absurde.
subst P.
eapply perp_col.
2:apply H.
assumption.
assumption.
induction (eq_dec_points Q R).
induction (eq_dec_points Q S).
subst R.
subst Q.
absurde.
subst Q.
eapply perp_col.
2:apply perp_left_comm.
2 :apply H.
assumption.
apply col_permutation_4.
assumption.
eapply perp_col.
2: apply perp_left_comm.
2: eapply perp_col.
3:apply H.
assumption.
assumption.
assumption.
eapply col_col.
apply perp_distinct in H.
spliter.
apply H.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma l9_4_1_aux : forall P Q A C R S M,
le S C R A ->
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> is_midpoint M R S ->
(forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
Proof.
intros.
induction (eq_dec_points R S).
subst S.
apply l7_3 in H5.
subst R.
unfold two_sides in H0.
spliter.
ex_and H8 T.
assert (T=M).
eapply inter_unicity.
apply col_permutation_1.
apply H8.
unfold Col.
right; left.
apply H9.
apply col_permutation_1.
assumption.
induction (eq_dec_points M P).
assert(Q <> M).
intro.
subst P.
subst Q.
apply perp_distinct in H2.
apply H0.
reflexivity.
assert(M <> Q).
intro.
apply H11.
subst Q.
reflexivity.
assert (Perp Q M A M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H2.
apply col_permutation_3.
assumption.
apply perp_left_comm in H13.
eapply perp_id in H13.
apply perp_in_comm in H13.
eapply perp_in_per in H13.
assert (Perp Q M C M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_3.
assumption.
apply perp_left_comm in H14.
eapply perp_id in H14.
apply perp_in_comm in H14.
eapply perp_in_per in H14.
eapply per_per_col.
apply l8_2.
apply H14.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
assert (Perp P M A M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H2.
apply col_permutation_1.
assumption.
apply perp_left_comm in H11.
eapply perp_id in H11.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
assert (Perp P M C M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H4.
apply col_permutation_1.
assumption.
apply perp_left_comm in H12.
eapply perp_id in H12.
apply perp_in_comm in H12.
eapply perp_in_per in H12.
eapply per_per_col.
apply l8_2.
apply H12.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
intro.
apply H7.
apply col_permutation_4.
assumption.
intro.
subst C.
apply between_identity in H9.
subst A.
apply H5.
assumption.
subst T.
split.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
intro.
subst C'.
apply l7_2 in H6.
eapply (midpoint_id _ _ M) in H6.
apply H10.
apply sym_equal.
apply H6.
apply l7_3_2.
induction H12.
assert (Bet U M C).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
unfold is_midpoint in H13.
spliter.
eapply l5_2.
apply H10.
assumption.
apply mid_bet.
assumption.
assert (Bet U M C).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply l5_2.
apply H10.
assumption.
unfold is_midpoint in H6.
spliter.
assumption.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst U.
eapply is_midpoint_id in H6.
subst C'.
apply H11.
reflexivity.
intro.
subst A.
apply perp_distinct in H2.
spliter.
apply H13.
reflexivity.
unfold is_midpoint in H6.
spliter.
assert (Bet A M C').
induction H12.
eapply outer_transitivity_between.
apply H9.
assumption.
intro.
apply H10.
subst C.
reflexivity.
eapply between_inner_transitivity.
apply H9.
assumption.
eapply l5_2.
apply H11.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
unfold le in H.
ex_and H D.
assert (C <> S).
intro.
subst S.
apply perp_distinct in H4.
spliter.
absurde.
assert (R <> D).
intro.
subst D.
apply cong_identity in H8.
apply H9.
subst S.
reflexivity.
assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert(exists M, is_midpoint M S R /\ is_midpoint M C D).
unfold two_sides in H0.
spliter.
ex_and H14 T.
eapply (l8_24 S R C A D T).
apply perp_sym.
apply perp_left_comm.
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
apply perp_right_comm.
apply perp_sym.
assumption.
eapply col_col.
apply H0.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.
ex_and H12 M'.
apply l7_2 in H12.
assert (M = M').
eapply l7_17.
apply H5.
apply H12.
subst M'.
split.
intro.
unfold out in H14.
spliter.
unfold out.
repeat split.
assumption.
eapply sym_preserve_diff.
2:apply H6.
apply H14.
assumption.
induction H16.
Focus 2.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
eapply between_exchange4.
apply H.
apply H16.
assert(Bet R U D \/ Bet R D U).
eapply l5_3.
apply H16.
assumption.
induction H17.
right.
eapply l7_15.
apply H5.
apply H6.
apply l7_2.
apply H13.
assumption.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
assumption.
unfold out.
intros.
spliter.
repeat split.
eapply sym_preserve_diff.
apply H15.
apply l7_2.
apply H6.
apply l7_2.
assumption.
intro.
subst R.
apply perp_distinct in H11.
spliter.
absurde.
induction H16.
eapply l5_1.
apply H10.
eapply l7_15.
apply l7_2.
apply H12.
apply H13.
apply l7_2.
apply H6.
assumption.
assumption.
left.
eapply between_exchange4.
eapply l7_15.
apply l7_2.
apply H12.
apply l7_2.
apply H6.
apply H13.
assumption.
assumption.
Qed.
Lemma per_col_eq : forall A B C, Per A B C -> Col A B C -> B <> C -> A = B.
Proof.
intros.
unfold Per in H.
ex_and H C'.
assert (Col A C C').
eapply col_col.
apply H1.
apply col_permutation_1.
assumption.
apply col_trivial_2.
unfold Col.
right; right.
apply between_symmetry.
apply mid_bet.
assumption.
assert (C = C' \/ is_midpoint A C C').
eapply l7_20.
apply col_permutation_4.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H.
contradiction.
eapply l7_17.
apply H4.
assumption.
Qed.
Lemma l9_4_1 : forall P Q A C R S M, two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> is_midpoint M R S -> (forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
intros.
assert (le S C R A \/ le R A S C).
apply le_cases.
induction H6.
apply (l9_4_1_aux P Q A C R S M); assumption.
assert((out R A U <-> out S C' C) -> (out R U A <-> out S C C')).
intro.
induction H7.
split.
intro.
eapply l6_6.
apply H7.
apply l6_6.
assumption.
intro.
apply l6_6.
apply H8.
apply l6_6.
assumption.
apply H7.
assert((out S C' C <-> out R A U) -> (out R A U <-> out S C' C)).
intro.
induction H8.
split.
intro.
apply H9.
assumption.
intro.
apply H8.
assumption.
apply H8.
eapply (l9_4_1_aux).
assumption.
apply l9_2.
apply H.
assumption.
assumption.
assumption.
assumption.
apply l7_2.
apply H4.
apply l7_2.
assumption.
Qed.
Lemma mid_two_sides : forall A B M X Y, A <> B -> is_midpoint M A B -> ~Col A B X -> is_midpoint M X Y -> two_sides A B X Y.
intros.
unfold two_sides.
repeat split.
assumption.
intro.
apply col_permutation_1 in H3.
contradiction.
intro.
apply H1.
unfold is_midpoint in *.
spliter.
assert (Col A M Y).
eapply col_transitivity_1.
apply H.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
assert (Col B M Y).
eapply col_transitivity_1.
intro.
apply H.
apply sym_equal.
apply H7.
unfold Col.
right; left.
assumption.
apply col_permutation_3.
assumption.
assert (Y <> M).
intro.
subst M.
apply cong_identity in H4.
subst Y.
apply H1.
apply col_permutation_1.
assumption.
assert (Col Y A X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
assert (Col Y B X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
assert (X <> Y).
intro.
subst Y.
apply between_identity in H2.
contradiction.
apply col_permutation_1.
eapply col_transitivity_1.
apply H11.
apply col_permutation_2.
assumption.
apply col_permutation_2.
assumption.
exists M.
unfold is_midpoint in *.
spliter.
split.
unfold Col.
right; right.
apply between_symmetry.
assumption.
assumption.
Qed.
Lemma col_preserves_two_sides : forall A B C D X Y, A <> B -> C <> D -> Col A B C -> Col A B D -> two_sides A B X Y -> two_sides C D X Y.
intros.
unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H4.
apply col_permutation_1.
eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
intro.
apply H5.
apply col_permutation_1.
eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
ex_and H6 T.
exists T.
split.
eapply col_col.
apply H3.
apply col_permutation_1.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma out_out_two_sides : forall A B X Y U V I, A <> B -> two_sides A B X Y -> Col I A B -> Col I X Y
-> out I X U -> out I Y V -> two_sides A B U V.
intros.
unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H5.
unfold out in H3.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
intro.
apply H6.
unfold out in H4.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
ex_and H7 T.
assert (I = T).
eapply inter_unicity.
apply col_permutation_1.
apply H1.
apply col_permutation_1.
apply H2.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
intro.
subst Y.
apply between_identity in H8.
subst X.
apply H5.
assumption.
subst I.
exists T.
split.
assumption.
unfold out in *.
spliter.
induction H12; induction H10.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
auto.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply between_inner_transitivity.
apply H13.
assumption.
assert (Bet U T Y).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
intro.
subst Y.
apply H6.
assumption.
assert (Bet V T X).
eapply between_exchange3.
apply between_symmetry.
apply H10.
apply between_symmetry.
assumption.
eapply between_exchange3.
apply between_symmetry.
apply H12.
apply between_symmetry.
assumption.
Qed.
Lemma out_out_two_sides1 : forall P Q A C M U V,
two_sides P Q A C -> Col M P Q -> Perp P Q A M ->
Perp P Q C M -> out M U A -> out M V C -> two_sides P Q U V.
intros.
eapply out_out_two_sides.
unfold two_sides in H.
spliter.
assumption.
apply H.
apply H0.
unfold two_sides in H.
spliter.
ex_and H7 T.
induction(eq_dec_points M P).
assert(M <> Q).
intro.
subst P.
subst Q.
absurde.
subst P.
apply perp_id in H1.
apply perp_in_comm in H1.
eapply perp_in_per in H1.
apply perp_id in H2.
apply perp_in_comm in H2.
eapply perp_in_per in H2.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H1.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
assert (Perp M P A M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H1.
apply col_permutation_1.
assumption.
assert(Perp M P C M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H2.
apply col_permutation_1.
assumption.
apply perp_id in H10.
apply perp_id in H11.
apply perp_in_comm in H10.
eapply perp_in_per in H10.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H10.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
apply l6_6.
assumption.
apply l6_6.
assumption.
Qed.
Lemma mid_preserves_col : forall A B C A' B' C' M, Col A B C -> is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
-> Col A' B' C'.
intros.
unfold Col in *.
induction H.
left.
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
induction H.
right; left.
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
right; right.
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
Qed.
Lemma l9_4_2_aux : forall P Q A C R S U V, le S C R A ->
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.
induction (eq_dec_points R S).
subst S.
eapply out_out_two_sides1.
apply H0.
apply H1.
assumption.
assumption.
assumption.
assumption.
assert(P <> Q).
apply perp_distinct in H4.
spliter.
assumption.
assert (two_sides R S A C).
eapply (col_preserves_two_sides P Q).
assumption.
apply H7.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
eapply (col_preserves_two_sides R S).
assumption.
assumption.
eapply col_permutation_1.
eapply col2.
apply H8.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.
assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert (Perp R S C S).
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert (HH9:=H9).
unfold two_sides in HH9.
spliter.
ex_and H15 T.
unfold le in H.
ex_and H C'.
assert (exists M, is_midpoint M S R /\ is_midpoint M C C').
eapply (l8_24 S R C A C' T).
apply perp_sym.
apply perp_left_comm.
assumption.
apply
perp_sym.
apply perp_left_comm.
assumption.
apply col_permutation_3.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.
ex_and H18 M.
double U M U'.
assert (R <> U).
intro.
subst U.
unfold out in H5.
spliter.
absurde.
assert (two_sides R S U U').
eapply mid_two_sides.
assumption.
apply l7_2.
apply H18.
intro.
apply H13.
eapply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply col_permutation_5.
assumption.
induction H5.
spliter.
induction H24.
unfold Col.
left.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
assumption.
apply l9_2.
eapply l9_3.
apply l9_2.
apply H22.
unfold Col.
right; right.
apply mid_bet.
apply H18.
apply l7_2.
assumption.
apply col_trivial_3.
assert (forall X Y, is_midpoint M X Y -> (out R X A <-> out S C Y)).
eapply l9_4_1.
apply H9.
apply col_trivial_1.
assumption.
apply col_trivial_3.
assumption.
apply l7_2.
assumption.
assert (out R U A <-> out S C U').
eapply H23.
assumption.
destruct H24.
eapply l6_7.
apply l6_6.
apply H24.
assumption.
apply l6_6.
assumption.
Qed.
Lemma l9_4_2 : forall P Q A C R S U V,
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.
assert( le S C R A \/ le R A S C).
apply le_cases.
induction H6.
eapply l9_4_2_aux.
apply H6.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
apply l9_2.
eapply l9_4_2_aux.
apply H6.
apply l9_2.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma l9_5 : forall P Q A C R B,
two_sides P Q A C -> Col R P Q -> out R A B -> two_sides P Q B C.
intros.
assert (P <> Q).
unfold two_sides in H.
spliter.
assumption.
assert(exists A0, Col P Q A0 /\ Perp P Q A A0).
eapply l8_18_existence.
intro.
unfold two_sides in H.
spliter.
apply H4.
apply col_permutation_2.
assumption.
assert(exists C0, Col P Q C0 /\ Perp P Q C C0).
eapply l8_18_existence.
unfold two_sides in H.
spliter.
intro.
apply H5.
apply col_permutation_2.
assumption.
assert(exists B0, Col P Q B0 /\ Perp P Q B B0).
eapply l8_18_existence.
assert (HH1:=H1).
unfold out in HH1.
unfold two_sides in H.
spliter.
intro.
assert (Col P B R).
eapply col2.
apply H.
assumption.
apply col_permutation_1.
assumption.
assert (R <> B).
intro.
subst B.
absurde.
assert(Col R P A ).
eapply col2.
apply H13.
eapply col_permutation_3.
assumption.
apply col_permutation_5.
apply out_col.
assumption.
apply H8.
eapply col_permutation_2.
eapply col2.
apply H.
apply col_trivial_2.
eapply colx.
assumption.
3:apply col_permutation_1.
3:apply H0.
3: apply H11.
assumption.
assumption.
apply col_permutation_5.
apply out_col.
assumption.
ex_and H3 A'.
ex_and H4 C'.
ex_and H5 B'.
assert (exists M, is_midpoint M A' C').
apply midpoint_existence.
ex_and H9 M.
double A M D.
assert (out C' D C <-> out A' A A).
eapply l9_4_1.
apply l9_2.
apply H.
apply col_permutation_2.
assumption.
assumption.
apply col_permutation_2.
assumption.
assumption.
apply l7_2.
apply H10.
apply l7_2.
assumption.
destruct H11.
assert (out C' D C).
apply H12.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.
assert (two_sides P Q A D).
eapply l9_4_2.
apply H.
apply col_permutation_2.
apply H3.
assumption.
apply col_permutation_2.
apply H4.
apply H7.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.
assumption.
assert (two_sides P Q B D).
eapply l9_3.
apply H14.
2:apply H9.
2: apply H0.2:assumption.
induction (eq_dec_points A' C').
subst C'.
apply l7_3 in H10.
subst A'.
apply col_permutation_2.
assumption.
eapply col_permutation_2.
eapply colx.
assumption.
apply H15.
intro.
subst C'.
eapply l7_2 in H10.
eapply midpoint_id in H10.
apply H15.
apply sym_equal.
apply H10.
apply l7_3_2.
assumption.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
try assumption.
eapply l9_4_2.
apply H15.
2: apply H8.
apply col_permutation_2.
assumption.
apply col_permutation_2.
apply H4.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst D.
unfold out in H13.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H7.
apply col_permutation_5.
apply out_col.
assumption.
eapply out_trivial.
intro.
subst B.
apply perp_distinct in H8.
spliter.
absurde.
apply l6_6.
assumption.
Qed.
Lemma outer_pasch : forall A B C P Q,
Bet A C P -> Bet B Q C -> exists X, Bet A X B /\ Bet P Q X.
Proof.
intros.
induction(classic (Col P Q C)).
induction(classic (Bet P Q C)).
exists A.
split.
apply between_symmetry.
apply between_trivial.
eapply between_exchange4.
apply H2.
apply between_symmetry.
assumption.
assert (out Q P C).
eapply l6_4_2.
split;trivial.
exists B.
split.
apply between_trivial.
unfold out in H3.
spliter.
induction H5.
eapply between_exchange3.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
eapply outer_transitivity_between2.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
assumption.
induction (eq_dec_points B Q).
subst Q.
exists B.
split; apply between_trivial.
assert (A <> P).
intro.
subst P.
apply between_identity in H.
subst C.
apply False_ind.
apply H1.
apply col_trivial_3.
assert (P <> Q).
intro.
subst Q.
apply H1.
apply col_trivial_1.
assert (P <> B).
intro.
subst P.
apply H1.
unfold Col.
left.
assumption.
assert(two_sides P Q C B).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
apply col_permutation_1.
assumption.
intro.
apply H1.
assert (Col B P C ).
eapply col2.
apply H2.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
eapply col2.
apply H5.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
exists Q.
split.
apply col_trivial_3.
apply between_symmetry.
assumption.
assert (two_sides P Q A B).
eapply l9_5.
apply H6.
apply col_trivial_1.
unfold out.
repeat split.
intro.
subst P.
apply H1.
apply col_trivial_3.
assumption.
left.
apply between_symmetry.
assumption.
unfold two_sides in H7.
spliter.
ex_and H10 X.
exists X.
split.
assumption.
assert (exists T, Bet X T P /\ Bet C T B).
eapply inner_pasch.
apply between_symmetry.
apply H11.
apply between_symmetry.
assumption.
ex_and H12 T.
assert (T = Q).
eapply inter_unicity.
unfold Col.
right; left.
apply H12.
unfold Col.
right; left.
apply H13.
apply col_permutation_4.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H9.
eapply col_permutation_2.
eapply col2.
2: apply col_permutation_4.
2:apply H10.
intro.
subst X.
apply H8.
eapply colx.
assumption.
3: unfold Col.
3:right; left.
3:apply between_symmetry.
3:apply H.
3: unfold Col.
3: left.
3: apply H11.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H12.
subst P.
apply H1.
apply col_trivial_3.
intro.
subst Q.
unfold two_sides in H6.
spliter.
apply H15.
apply col_trivial_3.
unfold Col.
right; left.
assumption.
apply col_permutation_5.
assumption.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H0.
subst Q.
apply H1.
apply col_trivial_2.
subst T.
apply between_symmetry.
assumption.
Qed.
Definition one_side := fun P Q A B =>
exists C, two_sides P Q A C /\ two_sides P Q B C.
Lemma l9_8_1 : forall P Q A B C, two_sides P Q A C -> two_sides P Q B C -> one_side P Q A B.
intros.
unfold one_side.
exists C.
split; assumption.
Qed.
Lemma not_two_sides_id : forall A P Q, ~ two_sides P Q A A.
intros.
intro.
unfold two_sides in H.
spliter.
ex_and H2 T.
apply between_identity in H3.
subst T.
apply H0.
apply H2.
Qed.
Lemma l9_8_2 : forall P Q A B C, two_sides P Q A C -> (one_side P Q A B -> two_sides P Q B C).
intros.
unfold one_side in H0.
ex_and H0 D.
assert (HH:= H).
assert (HH0:=H0).
assert (HH1:=H1).
unfold two_sides in HH.
unfold two_sides in HH0.
unfold two_sides in HH1.
spliter.
ex_and H13 T.
ex_and H9 X.
ex_and H5 Y.
assert (exists M , Bet Y M A /\ Bet X M B).
eapply inner_pasch.
apply H16.
apply H15.
ex_and H17 M.
assert (A <> D).
intro.
subst D.
apply not_two_sides_id in H0.
assumption.
assert (B <> D).
intro.
subst D.
apply not_two_sides_id in H1.
assumption.
induction (classic(Col A B D)).
induction (eq_dec_points M Y).
subst M.
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
apply col_permutation_3.
assumption.
apply bet_col in H16.
Col.
intro.
Col.
auto.
subst Y.
eapply l9_5.
apply H.
apply H9.
unfold out.
repeat split.
intro.
subst X.
apply H11.
assumption.
intro.
subst X.
apply H3.
assumption.
unfold Col in H21.
induction H21.
right.
eapply between_exchange3.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
induction H21.
assert (Bet D B A \/ Bet D A B).
eapply (l5_1 _ X).
intro.
subst X.
apply H4.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
induction H22.
assert (D = B).
eapply between_egality.
apply H22.
apply H21.
subst D.
absurde.
assert (D = A).
eapply between_egality.
apply H22.
apply between_symmetry.
assumption.
subst D.
absurde.
eapply (l5_2 D).
intro.
subst X.
apply H8.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
induction (eq_dec_points M X).
subst M.
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
Col.
apply bet_col in H16.
Col.
intro.
apply H4.
apply col_permutation_4.
assumption.
auto.
subst Y.
absurde.
eapply (l9_5 _ _ M _ X).
eapply l9_5.
apply H.
apply H5.
unfold out.
repeat split.
intro.
subst Y.
apply between_identity in H17.
subst M.
absurde.
assumption.
right.
assumption.
assumption.
unfold out.
assert (out Y M A).
unfold out.
repeat split.
assumption.
intro.
subst Y.
apply H11.
assumption.
left.
assumption.
repeat split.
assumption.
intro.
subst X.
apply between_identity in H18.
subst M.
absurde.
left.
apply H18.
eapply (l9_5 _ _ M).
eapply l9_5.
apply H.
apply H5.
unfold out.
repeat split.
intro.
subst Y.
apply H7.
assumption.
intro.
subst Y.
assert(Col B D X).
eapply (col2 _ M).
intro.
subst M.
apply H3.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ X).
intro.
subst X.
apply H4.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
right.
assumption.
apply H9.
unfold out.
repeat split.
intro.
subst X.
assert (Col A D Y).
eapply (col2 _ M).
intro.
subst M.
apply H7.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ Y).
intro.
subst Y.
apply H4.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
intro.
subst X.
apply H3.
assumption.
left.
assumption.
Qed.
Lemma l9_9 : forall P Q A B, two_sides P Q A B -> ~ one_side P Q A B.
intros.
intro.
assert(L:=l9_8_2).
apply (L P Q A B B )in H.
apply not_two_sides_id in H.
assumption.
assumption.
Qed.
Lemma l9_9_bis : forall P Q A B, one_side P Q A B -> ~ two_sides P Q A B.
intros.
intro.
unfold one_side in H.
ex_and H C.
assert (one_side P Q A B).
eapply l9_8_1.
apply H.
assumption.
assert (~ one_side P Q A B).
apply l9_9.
assumption.
contradiction.
Qed.
Lemma l9_10 : forall P Q A,
P<>Q -> ~ Col A P Q -> exists C, two_sides P Q A C.
Proof.
intros.
double A P A'.
exists A'.
unfold two_sides.
repeat split.
assumption.
assumption.
intro.
apply H0.
eapply col_permutation_2.
eapply (col2 _ A').
intro.
subst A'.
apply l7_2 in H1.
eapply is_midpoint_id in H1.
subst A.
apply H0.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
Qed.
Lemma one_side_reflexivity : forall P Q A,
~ Col A P Q -> one_side P Q A A.
Proof.
intros.
unfold one_side.
double A P C.
exists C.
assert (two_sides P Q A C).
repeat split.
intro.
subst Q.
apply H.
apply col_trivial_2.
assumption.
intro.
apply H.
apply col_permutation_2.
eapply (col2 _ C).
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst A.
apply H.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
split; assumption.
Qed.
Lemma one_side_symmetry : forall P Q A B,
one_side P Q A B -> one_side P Q B A.
Proof.
unfold one_side.
intros.
ex_and H C.
exists C.
split; assumption.
Qed.
Lemma one_side_transitivity : forall P Q A B C,
one_side P Q A B -> one_side P Q B C -> one_side P Q A C.
Proof.
intros.
unfold one_side in *.
ex_and H X.
ex_and H0 Y.
exists X.
split.
assumption.
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H2.
eapply l9_8_1.
apply l9_2.
apply H0.
apply l9_2.
assumption.
Qed.
End T9.