Library parallel
Require Export angles.
Section T12.
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
| H:(le ?X1 ?X2 ?X3 ?X3) |- _ => apply le_zero in H; smart_subst X2
| H:(is_midpoint ?A ?A ?B) |- _ => apply is_midpoint_id in H; smart_subst A
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 coplanar := fun A B C D: Tpoint => True.
Definition Par_strict := fun A B C D =>
A<>B /\ C<>D /\ coplanar A B C D /\ ~ exists X, Col X A B /\ Col X C D.
Definition Par := fun A B C D =>
Par_strict A B C D \/ (A<>B /\ C<>D /\ Col A C D /\ Col B C D).
Lemma par_reflexivity : forall A B, A<>B -> Par A B A B.
Proof.
intros.
unfold Par.
unfold Par_strict.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
apply col_trivial_3.
Qed.
Lemma par_strict_irreflexivity : forall A B, ~ Par_strict A B A B.
Proof.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; apply col_trivial_1.
Qed.
Lemma par_strict_symmetry :forall A B C D, Par_strict A B C D -> Par_strict C D A B.
Proof.
unfold Par_strict.
intros.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; assumption.
Qed.
Lemma parallel_symmetry :forall A B C D, Par A B C D -> Par C D A B.
Proof.
unfold Par.
intros.
induction H.
left.
apply par_strict_symmetry.
assumption.
spliter.
right.
repeat split;try assumption.
eapply (col_transitivity_1 _ D).
assumption.
Col.
Col.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.
Qed.
Lemma parallel_left_comm : forall A B C D, Par A B C D -> Par B A C D.
unfold Par.
intros.
induction H.
left.
unfold Par_strict in *.
spliter.
repeat split.
auto.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; Col.
right.
spliter.
repeat split.
auto.
assumption.
Col.
Col.
Qed.
Lemma parallel_right_comm : forall A B C D, Par A B C D -> Par A B D C.
intros.
apply parallel_symmetry in H.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
Qed.
Lemma parallel_comm : forall A B C D, Par A B C D -> Par B A D C.
intros.
apply parallel_left_comm.
apply parallel_right_comm.
assumption.
Qed.
Lemma l12_6 : forall A B C D, Par_strict A B C D -> one_side A B C D.
intros.
unfold Par_strict in H.
spliter.
assert(HH:= not_two_sides_one_side A B C D H).
apply HH.
intro.
apply H2.
exists C.
split.
Col.
apply col_trivial_1.
intro.
apply H2.
exists D.
split.
Col.
apply col_trivial_3.
intro.
apply H2.
unfold two_sides in H3.
spliter.
ex_and H6 T.
exists T.
apply bet_col in H7.
split; Col.
Qed.
Lemma perp_perp_col : forall X Y Z A B, Perp X Y A B -> Perp X Z A B -> Col X Y Z.
intros.
induction(classic(Col A B X)).
induction(eq_dec_points X A).
subst A.
assert(X <> B).
apply perp_distinct in H.
spliter.
assumption.
apply perp_right_comm in H.
apply perp_perp_in in H.
apply perp_in_comm in H.
apply perp_in_per in H.
apply perp_right_comm in H0.
apply perp_perp_in in H0.
apply perp_in_comm in H0.
apply perp_in_per in H0.
apply col_permutation_2.
eapply (per_per_col).
apply H.
assumption.
assumption.
assert(Perp A X X Y ).
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.
assert(Perp A X X Z).
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.
apply col_permutation_2.
eapply (per_per_col _ _ A).
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.
assumption.
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.
assert(HH0:=H).
assert(HH1:=H0).
unfold Perp in H.
unfold Perp in H0.
ex_and H Y0.
ex_and H0 Z0.
assert(HH2:=H).
assert(HH3:=H2).
apply perp_in_col in H.
apply perp_in_col in H2.
spliter.
assert(Perp X Y0 A B).
eapply perp_col.
intro.
subst Y0.
contradiction.
apply HH0.
assumption.
assert(Perp X Z0 A B).
eapply perp_col.
intro.
subst Z0.
contradiction.
apply HH1.
assumption.
assert(Y0 = Z0).
eapply l8_18_unicity.
apply H1.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Z0.
eapply (col_transitivity_1 _ Y0).
intro.
subst Y0.
contradiction.
Col.
Col.
Qed.
Lemma perp_perp_col_col : forall X1 X2 Y1 Y2 A B, Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> Col X2 Y1 Y2.
intros.
assert(HH0:= H).
assert(HH1:= H0).
unfold Perp in HH0.
unfold Perp in HH1.
ex_and HH0 X0.
ex_and HH1 Y0.
induction(eq_dec_points X1 Y2).
subst Y2.
assert(Perp Y1 X1 A B).
eapply perp_col.
intro.
subst Y1.
apply perp_distinct in H0.
spliter.
absurde.
apply H0.
apply col_trivial_2.
apply col_permutation_1.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.
assert(Perp Y2 X1 A B).
eapply perp_col.
auto.
apply perp_left_comm.
apply H0.
Col.
assert(Perp X1 Y2 A B).
eapply perp_left_comm.
assumption.
induction(eq_dec_points X1 Y1).
subst Y1.
apply col_permutation_2.
eapply perp_perp_col.
apply H6.
assumption.
assert(Perp X1 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H5.
Col.
induction (eq_dec_points X2 Y1).
subst Y1.
apply col_trivial_1.
assert(Perp X2 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H.
apply col_permutation_2.
eapply perp_perp_col.
apply H8.
assumption.
induction (eq_dec_points X2 Y2).
subst Y2.
apply col_trivial_3.
assert(Perp Y2 X2 A B).
eapply perp_col.
auto.
apply H5.
apply col_permutation_2.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.
eapply perp_perp_col.
apply H10.
apply perp_left_comm.
assumption.
Qed.
Lemma l12_9 : forall A1 A2 B1 B2 C1 C2, coplanar A1 A2 B1 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 -> Par A1 A2 B1 B2.
Proof.
intros.
unfold Par.
unfold Par_strict.
assert(A1 <> A2 /\ C1 <> C2).
apply perp_distinct.
assumption.
assert(B1 <> B2 /\ C1 <> C2).
apply perp_distinct.
assumption.
spliter.
induction(classic(Col A1 B1 B2)).
right.
repeat split; try assumption.
eapply perp_perp_col_col.
apply H0.
apply H1.
assumption.
left.
repeat split.
assumption.
assumption.
intro.
ex_and H7 AB.
apply H6.
induction(eq_dec_points AB A1).
subst AB.
assumption.
assert(Perp A1 AB C1 C2).
eapply perp_col.
auto.
apply H0.
Col.
eapply perp_perp_col_col.
apply perp_left_comm.
apply H10.
assumption.
assumption.
Qed.
Lemma parallel_existence : forall A B P, A <> B -> exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.
Proof.
intros.
induction(classic(Col A B P)).
exists A.
exists B.
repeat split.
assumption.
apply par_reflexivity.
assumption.
Col.
assert(exists P', Col A B P' /\ Perp A B P P').
eapply l8_18_existence.
assumption.
ex_and H1 P'.
assert(P <> P').
intro.
subst P'.
contradiction.
induction(eq_dec_points P' A).
subst P'.
assert(exists Q, Per Q P A /\ Cong Q P A B /\ one_side A P Q B).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
Col.
ex_and H4 Q.
exists P.
exists Q.
assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.
repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.
apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.
assert(exists Q, Per Q P P' /\ Cong Q P A B /\ one_side P' P Q A).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
eapply (col_transitivity_1 _ P').
auto.
Col.
Col.
ex_and H5 Q.
exists P.
exists Q.
assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H6.
apply cong_identity in H6.
contradiction.
repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.
apply per_perp_in in H5.
apply perp_in_perp in H5.
induction H5.
apply perp_distinct in H5.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.
Qed.
Lemma par_not_col : forall A B C D X, Par_strict A B C D -> Col X A B -> ~Col X C D.
intros.
unfold Par_strict in H.
spliter.
intro.
apply H3.
exists X.
split; assumption.
Qed.
Lemma not_diff_eq : forall A B : Tpoint, ~ A <> B -> A = B.
intros.
induction(classic (A = B)).
assumption.
contradiction.
Qed.
Lemma not_not : forall P : Prop, ~~P -> P.
intros.
induction(classic P).
assumption.
contradiction.
Qed.
Lemma not_par_strict_inter_exists : forall A1 B1 A2 B2, ~Par_strict A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par_strict in H.
apply not_and in H.
induction H.
exists A2.
apply not_diff_eq in H.
subst B1.
split.
apply col_trivial_1.
apply col_trivial_3.
apply not_and in H.
induction H.
apply not_diff_eq in H.
subst B2.
exists A1.
split.
apply col_trivial_3.
apply col_trivial_1.
apply not_and in H.
induction H.
apply False_ind.
apply H.
unfold coplanar.
apply I.
apply not_not in H.
ex_and H X.
exists X.
split.
Col.
Col.
Qed.
Lemma not_par_inter_exists : forall A1 B1 A2 B2, ~Par A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par in H.
apply not_or in H.
spliter.
apply not_par_strict_inter_exists.
assumption.
Qed.
Lemma not_strict_par1 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
assert(exists X, Col X A B /\ Col X C D).
exists X.
split; Col.
contradiction.
spliter.
apply col_permutation_1.
eapply col_transitivity_1.
apply H2.
Col.
Col.
Qed.
Lemma not_strict_par2 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B D.
intros.
eapply not_strict_par1.
apply parallel_right_comm.
apply H.
apply H0.
Col.
Qed.
Lemma not_strict_par : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C /\ Col A B D.
intros.
split.
eapply not_strict_par1.
apply H.
apply H0.
assumption.
eapply not_strict_par2.
apply H.
apply H0.
assumption.
Qed.
Lemma not_par_not_col : forall A B C, A <> B -> A <> C -> ~Par A B A C -> ~Col A B C.
intros.
intro.
apply H1.
unfold Par.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
Col.
Qed.
Lemma not_par_inter_unicity : forall A B C D X Y, A <> B -> C <> D -> ~Par A B C D -> Col A B X -> Col C D X -> Col A B Y -> Col C D Y -> X = Y.
intros.
induction(eq_dec_points C Y).
subst Y.
induction (eq_dec_points C X).
subst X.
reflexivity.
eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
apply parallel_symmetry.
unfold Par.
right.
repeat split.
assumption.
assumption.
Col.
assert(Col A C X).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.
assert(Col A C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ X).
assumption.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ C).
intro.
subst C.
apply not_par_not_col in H1.
apply H1.
eapply (col_transitivity_1 _ _).
apply H6.
Col.
Col.
assumption.
assumption.
Col.
assumption.
assumption.
eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
unfold Par.
right.
repeat split; try assumption.
assert(Col A C Y).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.
assert(Col B C Y).
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.
assumption.
Qed.
Lemma not_par_two_sides : forall A B C D, A <> B -> C <> D -> ~Par A B C D -> exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y.
intros.
assert(HH:=H1).
apply not_par_inter_exists in H1.
ex_and H1 T.
induction(eq_dec_points C T).
subst T.
prolong D C Y D C.
exists D.
exists Y.
repeat split.
apply col_trivial_2.
apply bet_col in H3.
Col.
assumption.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
induction(eq_dec_points A C).
subst C.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
Col.
apply bet_col in H3.
Col.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
assert(Col Y A C).
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
assumption.
Col.
assert(Col A C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
apply bet_col in H3.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ _).
apply H5.
Col.
assumption.
exists C.
split; Col.
prolong C T Y C T.
exists C.
exists Y.
repeat split.
apply col_trivial_3.
eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col in H4.
assumption.
assumption.
intro.
assert(C=T).
eapply not_par_inter_unicity.
3:apply HH.
assumption.
assumption.
Col.
apply col_trivial_3.
assumption.
Col.
contradiction.
intro.
assert(Y= T).
eapply not_par_inter_unicity.
3: apply HH.
assumption.
assumption.
Col.
eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col.
assumption.
assumption.
Col.
subst Y.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.
exists T.
split.
Col.
assumption.
Qed.
Lemma not_par_other_side : forall A B C D P, A <> B -> C <> D -> ~Par A B C D -> ~Col A B P -> exists Q, Col C D Q /\ two_sides A B P Q.
intros.
assert(exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y).
apply not_par_two_sides.
assumption.
assumption.
assumption.
ex_and H3 X.
ex_and H4 Y.
induction(classic(two_sides A B P X)).
exists X.
split; assumption.
apply not_two_sides_one_side in H6.
exists Y.
split.
assumption.
eapply l9_8_2.
apply H5.
apply one_side_symmetry.
assumption.
assumption.
intro.
apply H2.
Col.
unfold two_sides in H5.
spliter.
assumption.
Qed.
Lemma inter_unicity_not_par : forall A B C D P, ~Col A B C -> Col A B P -> Col C D P -> ~Par A B C D.
intros.
intro.
unfold Par in H2.
induction H2.
unfold Par_strict in H2.
spliter.
apply H5.
exists P.
split; Col.
spliter.
apply H.
apply col_permutation_1.
eapply col_transitivity_1.
apply H3.
Col.
Col.
Qed.
Lemma par_strict_one_side : forall A B C D P, Par_strict A B C D -> Col C D P -> one_side A B C P.
Proof.
intros.
assert(HH:= H).
unfold Par_strict in HH.
spliter.
apply l12_6 in H.
unfold one_side in *.
ex_and H C'.
exists C'.
split.
assumption.
apply not_one_side_two_sides.
assumption.
intro.
apply H4.
exists P.
split; Col.
unfold two_sides in H.
spliter.
assumption.
intro.
apply H4.
unfold one_side in H6.
ex_and H6 P'.
assert(one_side A B P C').
eapply l9_8_1.
apply H6.
assumption.
assert(two_sides A B P C).
eapply l9_8_2.
apply l9_2.
apply H.
apply one_side_symmetry.
assumption.
unfold two_sides in H9.
spliter.
ex_and H12 T.
exists T.
split.
assumption.
induction(eq_dec_points C P).
subst P.
apply between_identity in H13.
subst T.
apply col_trivial_1.
eapply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
apply bet_col in H13.
Col.
Qed.
Lemma col_not_col_not_par : forall A B C D, (exists P, Col A B P /\ Col C D P) -> (exists Q, Col C D Q /\ ~Col A B Q) -> ~Par A B C D.
intros.
ex_and H P.
ex_and H0 Q.
intro.
unfold Par in H3.
induction H3.
unfold Par_strict in H3.
spliter.
apply H6.
exists P.
split; Col.
spliter.
apply H2.
eapply col3.
apply H4.
Col.
Col.
Col.
Qed.
Lemma par_distincts : forall A B C D, Par A B C D -> (Par A B C D /\ A <> B /\ C <> D).
intros.
split.
assumption.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
split; assumption.
spliter.
split; assumption.
Qed.
Lemma par_not_col_strict : forall A B C D P, Par A B C D -> Col C D P -> ~Col A B P -> Par_strict A B C D.
intros.
apply parallel_symmetry in H.
unfold Par in H.
induction H.
apply par_strict_symmetry.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H5 X.
apply H1.
assert(Col A C D).
eapply (col_transitivity_1 _ B).
assumption.
Col.
Col.
assert(Col B C D).
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.
Lemma par_strict_all_one_side : forall A B C D, Par_strict A B C D -> (forall P, Col C D P -> one_side A B C P).
intros.
eapply par_strict_one_side.
apply H.
assumption.
Qed.
Lemma all_one_side_par_strict : forall A B C D, C <> D -> (forall P, Col C D P -> one_side A B C P) -> Par_strict A B C D.
intros.
unfold Par_strict.
repeat split.
assert(HH:=H0 D (col_trivial_2 _ _)).
unfold one_side in HH.
ex_and HH C0.
unfold two_sides in H1.
spliter.
assumption.
assumption.
intro.
ex_and H1 X.
assert(HH:= H0 X (col_permutation_1 _ _ _ H2) ).
unfold one_side in HH.
ex_and HH M.
unfold two_sides in H4.
spliter.
contradiction.
Qed.
Lemma col_eq : forall A B X Y, A <> X -> Col A X Y -> Col B X Y -> ~Col A X B -> X = Y.
intros.
eapply inter_unicity.
apply col_trivial_2.
3: apply H0.
apply col_trivial_2.
apply H1.
intro.
apply H2.
Col.
assumption.
Qed.
Lemma par_col_par : forall A B C D D', C <> D' -> Par A B C D -> Col C D D' -> Par A B C D'.
intros.
unfold Par in *.
induction H0.
left.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H4.
ex_and H5 P.
exists P.
split.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
Col.
Col.
right.
spliter.
repeat split.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
Qed.
Lemma par_col2_par : forall A B C D E F, E <> F -> Par A B C D -> Col C D E -> Col C D F -> Par A B E F.
intros.
induction (eq_dec_points C E).
subst E.
eapply par_col_par.
assumption.
apply H0.
assumption.
eapply par_col_par.
assumption.
apply parallel_right_comm.
eapply par_col_par.
apply H3.
apply H0.
assumption.
apply col_permutation_2.
eapply col2.
apply par_distincts in H0.
spliter.
apply H5.
assumption.
assumption.
Qed.
Lemma par_strict_col2_par_strict : forall A B C D E F, E <> F -> Par_strict A B C D -> Col C D E -> Col C D F -> Par_strict A B E F.
intros.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H5.
ex_and H6 X.
exists X.
split.
assumption.
assert(Col C E F).
eapply col2.
apply H3.
assumption.
assumption.
assert(Col D E F).
eapply (col2 _ C).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.
Lemma parallel_unicity : forall A1 A2 B1 B2 C1 C2 P,
~ Col P A1 A2 ->
Par A1 A2 B1 B2 -> Col P B1 B2 ->
Par A1 A2 C1 C2 -> Col P C1 C2 ->
Col C1 B1 B2 /\ Col C2 B1 B2.
intros.
apply par_distincts in H0.
apply par_distincts in H2.
spliter.
assert(Par_strict A1 A2 B1 B2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
assert(Par_strict A1 A2 C1 C2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
induction(classic(Col C1 B1 B2 /\ Col C2 B1 B2)).
assumption.
apply not_and in H10.
assert(exists C', Col C1 C2 C' /\ two_sides B1 B2 A1 C').
apply not_par_other_side.
assumption.
assumption.
apply col_not_col_not_par.
exists P.
split; Col.
induction H10.
exists C1.
split.
apply col_trivial_3.
intro.
apply H10.
Col.
exists C2.
split.
apply col_trivial_2.
intro.
apply H10.
Col.
intro.
unfold Par_strict in H8.
spliter.
apply H14.
exists A1.
split.
apply col_trivial_1.
Col.
ex_and H11 C'.
assert(HH:=H12).
unfold two_sides in H12.
spliter.
ex_and H15 B.
double C' P C.
unfold is_midpoint in H17.
spliter.
assert(exists D, Bet B D C /\ Bet P D A1).
eapply inner_pasch.
apply H16.
apply between_symmetry.
assumption.
ex_and H19 D.
assert(C' <> P).
intro.
subst C'.
contradiction.
assert (Par A1 A2 C' P).
eapply par_col2_par.
assumption.
apply H2.
Col.
Col.
assert(Par_strict A1 A2 C' P).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
apply col_trivial_2.
intro.
apply H.
Col.
assert(B <> P).
intro.
subst B.
eapply (par_not_col _ _ _ _ A1) in H23.
apply H23.
apply bet_col in H16.
Col.
apply col_trivial_1.
assert(P <> C).
intro.
subst C.
apply cong_identity in H18.
subst C'.
absurde.
assert(Col B P B1).
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
assert(Col B P B2).
apply col_permutation_1.
eapply (col_transitivity_1 _ B1).
auto.
Col.
Col.
assert(Col C' P C1).
induction(eq_dec_points C' C1).
subst C1.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ ).
apply H5.
assumption.
Col.
assert(Col C P C1).
induction(eq_dec_points C' C1).
subst C1.
apply bet_col in H17.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.
assert(Col C' P C2).
induction(eq_dec_points C' C2).
subst C2.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
assert(Col C P C2).
induction(eq_dec_points C' C2).
subst C2.
apply bet_col in H17.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.
assert(~Col B P C).
intro.
assert(Col B P C').
apply col_permutation_2.
eapply col_transitivity_1.
apply H25.
apply bet_col in H17.
Col.
Col.
apply H14.
apply (col3 B P); assumption.
assert(P <> D).
intro.
subst D.
apply bet_col in H19.
contradiction.
assert(HE:=euclid P B C D A1 H20 H19 H33).
ex_and HE X.
ex_and H34 Y.
assert(Hx:= l12_6 A1 A2 P X).
induction(eq_dec_points P X).
subst X.
apply between_identity in H34.
subst B.
absurde.
assert(Par_strict A1 A2 P X).
eapply (par_strict_col2_par_strict _ _ B1 B2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply col3.
apply H24.
assumption.
assumption.
apply bet_col in H34.
Col.
apply Hx in H38.
assert(Hy:= l12_6 A1 A2 P Y).
induction(eq_dec_points P Y).
subst Y.
apply between_identity in H35.
subst C.
absurde.
assert(Par_strict A1 A2 P Y).
eapply (par_strict_col2_par_strict _ _ C1 C2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply (col3 C P).
auto.
assumption.
assumption.
apply bet_col in H35.
Col.
apply Hy in H40.
assert(one_side A1 A2 X Y).
eapply one_side_transitivity.
2:apply H40.
unfold one_side in H38.
unfold one_side.
ex_and H38 Z.
exists Z.
split.
assumption.
assumption.
assert(Ho:=H41).
unfold one_side in H41.
ex_and H41 Z.
unfold two_sides in H41.
unfold two_sides in H42.
spliter.
assert(two_sides A1 A2 X Y).
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists A1.
split.
apply col_trivial_1.
assumption.
apply l9_9 in H49.
contradiction.
Qed.
Lemma par_trans : forall A1 A2 B1 B2 C1 C2, Par A1 A2 B1 B2 -> Par B1 B2 C1 C2 -> Par A1 A2 C1 C2.
intros.
apply par_distincts in H.
apply par_distincts in H0.
spliter.
induction(classic(Par A1 A2 C1 C2)).
assumption.
apply not_par_inter_exists in H5.
ex_and H5 X.
induction(classic(Col X B1 B2)).
unfold Par in H, H0.
induction H.
eapply (par_not_col _ _ _ _ X) in H.
contradiction.
Col.
induction H0.
eapply (par_not_col _ _ _ _ X) in H0.
apply False_ind.
apply H0.
Col.
assumption.
spliter.
unfold Par.
right.
repeat split; try assumption.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
apply parallel_symmetry in H.
apply col_permutation_2 in H5.
apply col_permutation_2 in H6.
assert(HH:=parallel_unicity B1 B2 A1 A2 C1 C2 X H7 H H5 H0 H6).
spliter.
apply parallel_symmetry .
unfold Par.
right.
repeat split; try assumption.
Qed.
Definition inter A1 A2 B1 B2 X := (exists P, Col P B1 B2 /\ ~Col P A1 A2) /\ Col A1 A2 X /\ Col B1 B2 X.
Lemma inter_trivial : forall A B X, ~Col A B X -> inter A X B X X.
intros.
unfold inter.
split.
exists B.
split.
Col.
intro.
apply H.
Col.
split; Col.
Qed.
Lemma inter_sym : forall A B C D X, C <> D -> inter A B C D X -> inter C D A B X.
intros.
unfold inter in *.
spliter.
ex_and H0 P.
assert(A <> B).
intro.
subst B.
apply H3.
Col.
split.
induction(eq_dec_points A X).
treat_equalities.
exists B.
split.
Col.
intro.
apply H3.
eapply col3.
apply H.
Col.
Col.
Col.
exists A.
split.
Col.
intro.
apply H3.
assert(Col A P X).
eapply col3.
apply H.
Col.
Col.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H5.
Col.
Col.
split; assumption.
Qed.
Lemma inter_left_comm : forall A B C D X, inter A B C D X -> inter B A C D X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
assumption.
intro.
apply H2.
Col.
split; Col.
Qed.
Lemma inter_right_comm : forall A B C D X, inter A B C D X -> inter A B D C X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
Col.
assumption.
split; Col.
Qed.
Lemma inter_comm : forall A B C D X, inter A B C D X -> inter B A D C X.
intros.
apply inter_left_comm.
apply inter_right_comm.
assumption.
Qed.
Lemma l12_16 : forall A1 A2 B1 B2 C1 C2 X, Par A1 A2 B1 B2 -> inter A1 A2 C1 C2 X -> exists Y, inter B1 B2 C1 C2 Y.
intros.
assert(HH:= H).
unfold Par in H.
induction H.
unfold inter in H0.
spliter.
ex_and H0 P.
assert(~Col B1 B2 X).
intro.
unfold Par_strict in H.
spliter.
apply H7.
exists X.
auto with Col.
assert(HH1:= l8_18_existence B1 B2 X H4).
ex_and HH1 X0.
assert(~Par B1 B2 C1 C2).
intro.
assert(Par A1 A2 C1 C2).
eapply (par_trans _ _ B1 B2).
unfold Par.
left.
assumption.
assumption.
assert(~Par A1 A2 C1 C2).
apply col_not_col_not_par.
exists X.
auto with Col.
exists P.
auto with Col.
contradiction.
apply not_par_inter_exists in H7.
ex_and H7 Y.
exists Y.
split.
exists X.
split.
auto with Col.
intro.
apply H4.
auto with Col.
auto with Col.
unfold inter in H0.
spliter.
ex_and H0 P.
exists X.
split.
exists P.
split.
auto with Col.
intro.
apply H6.
eapply (col3 B1 B2); auto with Col.
split.
apply parallel_symmetry in HH.
unfold Par in HH.
induction HH.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists A1.
split.
auto with Col.
apply col_trivial_1.
spliter.
apply (col3 A1 A2); auto with Col.
auto with Col.
Qed.
Lemma l12_17 : forall A B C D P, A <> B -> is_midpoint P A C -> is_midpoint P B D -> Par A B C D.
intros.
induction(classic(Col A B P)).
unfold Par.
right.
induction(eq_dec_points A P).
subst P.
apply is_midpoint_id in H0.
subst C.
repeat split.
assumption.
intro.
treat_equalities.
apply l7_2 in H1.
apply is_midpoint_id in H1.
contradiction.
apply col_trivial_1.
unfold is_midpoint in H1.
spliter.
apply bet_col.
assumption.
induction(eq_dec_points B P).
subst P.
apply is_midpoint_id in H1.
subst D.
repeat split.
assumption.
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
auto.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0 .
Col.
apply col_trivial_3.
assert(HH0 := H0).
assert(HH1:= H1).
unfold is_midpoint in H0.
unfold is_midpoint in H1.
spliter.
apply bet_col in H1.
apply bet_col in H0.
assert(Col B C P).
eapply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
assert(Col B C D).
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.
repeat split.
assumption.
intro.
treat_equalities.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply HH0.
apply l7_2.
assumption.
contradiction.
induction(eq_dec_points A D).
subst D.
apply col_trivial_3.
assert(Col C D P).
eapply (col_transitivity_1 _ B).
intro.
subst C.
assert(A = D).
eapply midpoint_id.
eapply l7_2.
apply HH0.
assumption.
contradiction.
Col.
Col.
induction(eq_dec_points C P).
treat_equalities.
intuition.
apply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.
assumption.
assert(exists E, Col A B E /\ Perp A B P E).
eapply l8_18_existence.
assumption.
ex_and H3 E.
assert(A <> P).
intro.
treat_equalities.
apply H2.
apply col_trivial_3.
induction(eq_dec_points A E).
treat_equalities.
assert(Per P A B).
eapply perp_in_per.
apply perp_in_comm.
eapply perp_perp_in.
apply perp_sym.
apply perp_comm.
assumption.
prolong B A B' B A.
prolong B' P D' B' P.
assert(is_midpoint C D D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H0.
split.
apply H8.
Cong.
split.
assumption.
Cong.
assert(Per P A B').
eapply per_col.
apply H.
assumption.
apply bet_col in H6.
Col.
ex_and H3 B''.
assert(B' = B'').
eapply symmetric_point_unicity.
split.
apply H6.
Cong.
assumption.
subst B''.
assert(Cong P D P D').
apply (cong_transitivity _ _ B P).
unfold is_midpoint in H1.
spliter.
Cong.
apply (cong_transitivity _ _ B' P).
Cong.
Cong.
assert(Per P C D).
unfold Per.
exists D'.
split; assumption.
apply per_perp_in in H14.
apply perp_in_perp in H14.
induction H14.
apply perp_distinct in H14.
intuition.
eapply l12_9.
apply I.
apply H4.
apply perp_sym.
eapply perp_col.
auto.
apply H14.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0.
Col.
intro.
treat_equalities.
apply l7_2 in H0.
eapply is_midpoint_id in H0.
auto.
intro.
subst D.
assert(C = D').
apply is_midpoint_id.
assumption.
subst D'.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
prolong E P F E P.
assert(Col C D F).
eapply mid_preserves_col.
2: apply H0.
2:apply H1.
apply H3.
split.
assumption.
Cong.
prolong A E A' A E.
prolong A' P C' A' P.
assert(is_midpoint F C C').
eapply symmetry_preserves_midpoint.
apply H0.
split.
apply H7.
Cong.
split.
apply H12.
Cong.
split.
assumption.
Cong.
assert(Per P E A).
eapply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
Col.
assert(Cong P C P C').
eapply (cong_transitivity _ _ P A).
unfold is_midpoint in H0.
spliter.
Cong.
eapply (cong_transitivity _ _ P A').
unfold Per in H15.
ex_and H15 A''.
assert( A' = A'').
eapply symmetric_point_unicity.
split.
apply H10.
Cong.
assumption.
subst A''.
assumption.
Cong.
assert(Per P F C).
unfold Per.
exists C'.
split.
assumption.
assumption.
apply per_perp_in in H17.
apply perp_in_comm in H17.
apply perp_in_perp in H17.
induction H17.
eapply l12_9.
apply I.
apply H4.
eapply perp_col.
intro.
subst D.
assert (A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
treat_equalities.
apply perp_distinct in H17.
spliter.
auto.
apply perp_left_comm.
apply H17.
apply bet_col in H7.
Col.
Col.
apply perp_distinct in H17.
spliter.
tauto.
intro.
treat_equalities.
apply perp_distinct in H4.
spliter.
tauto.
intro.
subst C.
assert(F = C').
apply is_midpoint_id .
assumption.
treat_equalities.
assert(A = E).
eapply midpoint_id.
apply l7_2.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
tauto.
Qed.
Lemma l12_18_a : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par A B C D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
spliter.
eapply l12_17.
intro.
subst B.
apply H1.
apply col_trivial_1.
apply H5.
apply H6.
Qed.
Lemma l12_18_b : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par B C D A.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply l12_18_a.
assumption.
Cong.
intro.
apply H1.
assert(Col B C P).
eapply col_transitivity_1.
apply H2.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
apply H4.
Col.
Qed.
Lemma l12_18_c : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> two_sides B D A C.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
assert(Col A B P).
apply col_permutation_2.
eapply (col2 _ D).
assumption.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
apply H1.
assert(Col B P C).
eapply (col2 _ D).
assumption.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
exists P.
split.
Col.
spliter.
unfold is_midpoint in H5.
tauto.
Qed.
Lemma l12_18_d : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> two_sides A C B D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply (l12_18_c _ _ _ _ P).
Cong.
Cong.
intro.
apply H1.
assert(Col A B P).
eapply col_permutation_2.
eapply col2.
apply H2.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
contradiction.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
Qed.
Lemma l12_18 : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par A B C D /\ Par B C D A /\
two_sides B D A C /\ two_sides A C B D.
intros.
split.
apply (l12_18_a _ _ _ _ P); assumption.
split.
apply (l12_18_b _ _ _ _ P); assumption.
split.
apply (l12_18_c _ _ _ _ P); assumption.
apply (l12_18_d _ _ _ _ P); assumption.
Qed.
Lemma l12_19 : forall A B C D , ~Col A B C -> Par A B C D -> Par B C D A ->
Cong A B C D /\ Cong B C D A /\
two_sides B D A C /\ two_sides A C B D.
intros.
assert(exists P, is_midpoint P A C) by (eapply midpoint_existence).
ex_and H2 P.
double B P D'.
assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.
assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_1.
apply H3.
assumption.
assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H0.
apply H6.
assert(Col C D D').
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists C.
split; apply col_trivial_1.
spliter.
Col.
assert(Par B C D' A).
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_2.
apply H2.
apply l7_2.
assumption.
assert(Par D A D' A).
eapply par_trans.
apply parallel_symmetry.
apply H1.
assumption.
assert(Col A D D').
unfold Par in H10.
induction H10.
unfold Par_strict in H10.
spliter.
apply False_ind.
apply H13.
exists A.
split; apply col_trivial_3.
spliter.
Col.
assert(D = D').
eapply inter_unicity.
3: apply H11.
apply col_trivial_2.
2: apply H8.
apply col_trivial_2.
intro.
apply H.
assert(Col P C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ A).
intro.
subst C.
apply H.
apply col_trivial_3.
Col.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.
assert(Col P C D').
apply col_permutation_2.
eapply (col2 _ D).
apply par_distincts in H0.
spliter.
assumption.
Col.
Col.
assert(Col P A D').
eapply (col2 _ C).
intro.
subst P.
apply l7_2 in H3.
apply is_midpoint_id in H3.
subst C.
apply H.
apply col_trivial_3.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.
assumption.
eapply (col3 P D').
intro.
subst D'.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P.
apply H.
unfold is_midpoint in H3.
spliter.
apply bet_col.
assumption.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply par_distincts in H0.
spliter.
assumption.
subst D'.
split.
Cong.
split.
Cong.
assert(B <> D).
intro.
subst D.
apply l7_3 in H2.
subst P.
apply H.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply False_ind.
apply H13.
exists B.
split; apply col_trivial_3.
spliter.
Col.
unfold is_midpoint in *.
spliter.
split.
eapply l12_18_c.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.
eapply l12_18_d.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.
Qed.
Lemma par_two_sides_two_sides : forall A B C D, Par A B C D -> two_sides B D A C -> two_sides A C B D.
intros.
apply par_distincts in H.
spliter.
unfold Par in H.
induction H.
Focus 2.
unfold two_sides in H0.
spliter.
apply False_ind.
apply H3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.
assert(A <> C).
intro.
subst C.
unfold Par_strict in H.
spliter.
apply H5.
exists A.
split; apply col_trivial_1.
unfold two_sides in *.
spliter.
ex_and H6 T.
repeat split.
assumption.
intro.
assert(Col T B C).
apply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
apply bet_col in H7.
Col.
Col.
apply H5.
apply col_permutation_2.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists C.
split.
Col.
apply col_trivial_1.
Col.
Col.
intro.
assert(Col T C D).
apply col_permutation_2.
apply (col_transitivity_1 _ A).
auto.
Col.
apply bet_col in H7.
Col.
apply H5.
apply col_permutation_1.
apply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists A.
split.
apply col_trivial_1.
Col.
Col.
Col.
exists T.
split.
apply bet_col in H7.
Col.
unfold Col in H6.
induction H6.
assert(HH:= outer_pasch C D T A B (between_symmetry _ _ _ H7) (between_symmetry _ _ _ H6)).
ex_and HH X.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.
induction H6.
assert(HH:= outer_pasch A B T C D H7 H6).
ex_and HH X.
apply False_ind.
unfold Par_strict in H.
spliter.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.
apply between_symmetry.
assumption.
Qed.
Lemma out_one_side : forall A B C D X, A <> B -> ~ Col A B C -> Col A B X -> out X C D -> one_side A B C D.
intros.
induction (eq_dec_points C D).
subst D.
apply one_side_reflexivity.
intro.
apply H0.
Col.
prolong C X C' C X.
exists C'.
assert(two_sides A B C C').
unfold two_sides.
repeat split.
assumption.
intro.
apply H0.
Col.
intro.
assert(C'=X).
eapply (inter_unicity A B C D).
Col.
apply out_col in H2.
eapply (col_transitivity_1 _ X).
intro.
treat_equalities.
contradiction.
Col.
apply bet_col in H4.
Col.
assumption.
apply out_col in H2.
Col.
intro.
apply H0.
Col.
assumption.
treat_equalities.
unfold out in H2.
tauto.
exists X.
split; Col.
assert(two_sides A B D C').
eapply (l9_5 _ _ _ _ X).
apply H6.
Col.
assumption.
split; assumption.
Qed.
Lemma l12_20_bis : forall A B C D, Par A B C D -> Cong A B C D -> two_sides B D A C ->
Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.
induction(eq_dec_points B C).
subst C.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_1.
induction(eq_dec_points A D).
subst D.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_3.
assert(~ Col A B C).
intro.
assert(Col A B D).
eapply not_strict_par1.
2: apply H4.
2: apply col_trivial_2.
apply parallel_right_comm.
assumption.
unfold two_sides in H1.
spliter.
contradiction.
assert(exists P, is_midpoint P A C) by (apply midpoint_existence).
ex_and H5 P.
double B P D'.
assert(Par B C D' A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.
assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H4.
apply col_trivial_1.
apply H6.
assumption.
assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.
assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H.
assumption.
assert(Col C D D').
unfold Par in H11.
induction H11.
unfold Par_strict in H11.
spliter.
apply False_ind.
apply H14.
exists C.
split; apply col_trivial_1.
spliter.
Col.
assert(Cong C D C D').
eapply (cong_transitivity _ _ A B).
Cong.
Cong.
assert(D = D' \/ is_midpoint C D D').
eapply l7_20.
Col.
assumption.
induction H14.
subst D'.
assert(Par B C D A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.
split.
assumption.
assert(HH:=l12_19 A B C D H4 H H14).
spliter.
split; assumption.
assert(two_sides A C B D).
apply par_two_sides_two_sides.
assumption.
assumption.
assert(HH:= H15).
assert(HH1:=H1).
unfold two_sides in H15, H1.
spliter.
ex_and H21 T.
ex_and H18 T'.
assert(T = T').
apply bet_col in H22.
apply bet_col in H23.
eapply (inter_unicity A C B D); Col.
subst T'.
assert(~Col B C T).
intro.
apply H16.
apply col_permutation_1.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
apply H20.
apply bet_col in H23.
Col.
Col.
Col.
assert(one_side B C T D).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_3.
apply bet_out in H23.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_3.
auto.
assert(one_side B C T A).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_2.
apply between_symmetry in H22.
apply bet_out in H22.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_2.
assumption.
assert(one_side B C A D).
apply (one_side_transitivity _ _ _ T).
apply one_side_symmetry.
assumption.
assumption.
assert(two_sides B C D D').
unfold two_sides.
repeat split.
assumption.
intro.
apply H20.
Col.
intro.
apply H20.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply H17.
apply col_trivial_3.
Col.
Col.
exists C.
split.
apply col_trivial_3.
unfold is_midpoint in H14.
spliter.
assumption.
assert(two_sides B C A D').
eapply l9_8_2.
apply H28.
apply one_side_symmetry.
assumption.
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H32.
unfold two_sides in H29.
spliter.
ex_and H35 X.
exists X.
split.
assumption.
apply bet_col in H36.
Col.
spliter.
apply False_ind.
apply H4.
eapply (col_transitivity_1 _ P).
intro.
subst P.
apply is_midpoint_id in H6.
tauto.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply l7_3 in H5.
subst P.
apply H4.
unfold is_midpoint in H6.
spliter.
auto.
apply bet_col.
assumption.
Col.
unfold is_midpoint in H5.
spliter.
apply bet_col in H5.
Col.
unfold is_midpoint in H6.
spliter.
apply bet_col in H6.
Col.
Qed.
Lemma l12_20 : forall A B C D, Par A B C D -> Cong A B C D -> two_sides A C B D ->
Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.
assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.
assert(HH:=l12_20_bis A B C D H H0 H2).
spliter.
split.
assumption.
split.
assumption.
assumption.
Qed.
Lemma par_one_or_two_sides : forall A B C D, Par_strict A B C D
-> two_sides A C B D /\ two_sides B D A C \/ one_side A C B D /\ one_side B D A C.
intros.
induction(classic (two_sides A C B D)).
left.
split.
assumption.
apply par_two_sides_two_sides.
apply parallel_comm.
unfold Par.
left.
assumption.
assumption.
right.
assert(HH:=H).
unfold Par_strict in H.
spliter.
assert(A <> C).
intro.
subst C.
apply H3.
exists A.
split; Col.
assert(B <> D).
intro.
subst D.
apply H3.
exists B.
split; Col.
split.
apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists C.
split; Col.
intro.
apply H3.
exists A.
split; Col.
assumption.
apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists D.
split; Col.
intro.
apply H3.
exists B.
split; Col.
intro.
apply H0.
apply par_two_sides_two_sides.
left.
assumption.
assumption.
Qed.
Lemma l12_21_a : forall A B C D, two_sides A C B D -> (Par A B C D -> Conga B A C D C A).
intros.
assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.
assert(B <> C).
intro.
subst B.
unfold two_sides in H.
spliter.
apply H2.
apply col_trivial_3.
assert(~Col B C D).
unfold two_sides in H1.
spliter.
intro.
apply H4.
Col.
assert(inter B C D C C).
repeat split.
exists D.
split.
apply col_trivial_1.
intro.
apply H3.
Col.
apply col_trivial_2.
apply col_trivial_2.
assert(HH:= parallel_existence B C A H2).
ex_and HH X.
ex_and H5 Y.
assert(HH:=l12_16 B C X Y D C C H6 H4).
ex_and HH D'.
apply par_distincts in H0.
spliter.
assert(~Col A B C).
intro.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.
exists C.
split; Col.
spliter.
contradiction.
assert(Par B C A D').
eapply par_col2_par.
intro.
subst D'.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.
unfold inter in H7.
ex_and H8 P.
exists A.
split; Col.
spliter.
contradiction.
apply H6.
Col.
unfold inter in H8.
spliter.
assumption.
assert(Par_strict A B C D).
unfold Par in H0.
induction H0.
assumption.
spliter.
apply False_ind.
apply H11.
apply col_permutation_1.
eapply (col2 _ D).
assumption.
Col.
Col.
assert(Par_strict B C A D').
unfold Par in H12.
induction H12.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H17 P.
apply H11.
eapply col2.
apply H14.
Col.
Col.
assert(Par A B C D').
eapply par_col_par.
intro.
subst D'.
unfold Par_strict in H14.
spliter.
apply H17.
exists C.
split; Col.
apply H0.
unfold inter in H8.
spliter.
Col.
apply parallel_right_comm in H12.
assert(HH:= l12_19 A B C D' H11 H15 H12).
spliter.
assert(A <> C).
unfold two_sides in H19.
spliter.
assumption.
assert(Conga B A C D' C A).
apply cong3_conga.
auto.
auto.
repeat split; Cong.
eapply l11_10.
apply H21.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold inter in H8.
spliter.
induction H23.
assert(one_side A C D D').
eapply l9_8_1.
apply l9_2.
apply H.
apply l9_2.
assumption.
assert(two_sides A C D D').
unfold two_sides.
repeat split.
assumption.
unfold two_sides in H.
spliter.
assumption.
unfold two_sides in H19.
spliter.
assumption.
exists C.
split.
apply col_trivial_3.
assumption.
apply l9_9 in H25.
contradiction.
induction H23.
apply bet_out in H23.
apply l6_6.
assumption.
intro.
treat_equalities.
auto.
auto.
apply between_symmetry in H23.
apply bet_out in H23.
assumption.
auto.
intro.
treat_equalities.
auto.
apply out_trivial.
auto.
Qed.
Lemma midpoint_preserves_out : forall A B C A' B' C' M, out A B C ->
is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
-> out A' B' C'.
intros.
unfold out in H.
spliter.
unfold out.
repeat split.
intro.
subst B'.
assert (A = B).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
intro.
subst C'.
assert (A = C).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
induction H4.
left.
apply (l7_15 A B C A' B' C' M); assumption.
right.
eapply (l7_15 A C B A' C' B' M); assumption.
Qed.
Lemma l12_21_b : forall A B C D, two_sides A C B D -> (Conga B A C D C A -> Par A B C D).
intros.
apply conga_diff in H0.
spliter.
assert(~Col A B C).
intro.
unfold two_sides in H.
spliter.
apply col_permutation_4 in H5.
assert(Col D C A).
eapply col_conga_col.
apply H5.
assumption.
contradiction.
assert(A <> B /\ C <> D).
auto.
spliter.
assert(HH:=segment_construction_3 C D A B H7 H6).
ex_and HH D'.
assert(Conga B A C D' C A).
eapply l11_10.
apply H0.
apply out_trivial.
assumption.
apply out_trivial.
assumption.
apply l6_6.
assumption.
apply out_trivial.
assumption.
assert(Cong D' A B C).
eapply cong2_conga_cong.
apply conga_sym.
apply H10.
Cong.
Cong.
assert(two_sides A C D' B).
eapply l9_5.
apply l9_2.
apply H.
apply col_trivial_3.
assumption.
unfold two_sides in H12.
spliter.
ex_and H15 M.
assert(B <> D').
intro.
treat_equalities.
contradiction.
assert(is_midpoint M A C /\ is_midpoint M B D').
apply l7_21.
assumption.
assumption.
Cong.
Cong.
Col.
apply bet_col in H16.
Col.
spliter.
assert(Par A B C D').
eapply l12_17.
assumption.
apply H18.
assumption.
eapply par_col_par.
auto.
apply H20.
apply out_col in H8.
Col.
Qed.
Lemma l12_21 : forall A B C D , two_sides A C B D -> (Conga B A C D C A <-> Par A B C D).
intros.
split.
intro.
apply l12_21_b ; assumption.
intro.
apply l12_21_a; assumption.
Qed.
Lemma par_id : forall A B C, Par A B A C -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H2.
exists A.
split; Col.
spliter.
Col.
Qed.
Lemma not_par_strict_id : forall A B C, ~ Par_strict A B A C.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; Col.
Qed.
Lemma l6_7_1 : forall A B C D, out A B C -> out A B D -> out A C D.
intros.
unfold out in *.
spliter.
repeat split.
assumption.
assumption.
induction H4; induction H2.
eapply l5_1.
2: apply H4.
auto.
assumption.
right.
eapply between_exchange4.
apply H2.
assumption.
left.
eapply between_exchange4.
apply H4.
assumption.
eapply l5_3.
apply H4.
apply H2.
Qed.
Lemma l12_22_a : forall A B C D P, out P A C -> one_side P A B D -> Par A B C D -> Conga B A P D C P.
intros.
unfold Par in H1.
induction H1.
assert(~Col A B C).
intro.
unfold Par_strict in H1.
spliter.
apply H5.
exists C.
split; Col.
assert( A <> C).
intro.
treat_equalities.
assert(HH := not_par_strict_id A B D).
contradiction.
assert(HH:= parallel_existence A C B H3).
ex_and HH X.
ex_and H4 Y.
assert(inter A C C D C).
apply inter_right_comm.
apply inter_trivial.
intro.
unfold Par_strict in H1.
spliter.
apply H10.
exists A.
split; Col.
assert(HH:= l12_16 A C X Y C D C H5 H7).
ex_and HH D'.
assert(Par A C B D').
eapply par_col2_par.
intro.
unfold Par_strict in H1.
spliter.
unfold inter in H8.
spliter.
treat_equalities.
apply H12.
exists B.
split; Col.
apply H5.
Col.
unfold inter in H8.
spliter.
assumption.
assert(Par A B C D').
eapply par_col_par.
intro.
treat_equalities.
apply H2.
apply parallel_comm in H9.
apply par_id in H9.
Col.
unfold Par.
left.
apply H1.
unfold inter in H8.
spliter.
assumption.
assert(Par_strict A C B D').
unfold Par in H9.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.
assert(Cong A B D' C /\
Cong B D' C A /\ two_sides B C A D' /\ two_sides A D' B C).
eapply l12_19.
eapply par_not_col.
apply H11.
Col.
apply parallel_right_comm.
assumption.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
spliter.
prolong C A C' C A.
assert(Par B D' A C').
eapply par_col_par.
intro.
treat_equalities.
tauto.
unfold Par.
left.
apply par_strict_symmetry.
apply H11.
apply bet_col in H16.
Col.
assert(Cong B D' A C').
eCong.
assert(Par_strict A B C D').
unfold Par in H10.
induction H10.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
tauto.
Col.
Col.
assert(HH := l12_6 A B C D' H20).
assert(two_sides A B C C').
unfold two_sides.
repeat split.
intro.
treat_equalities.
apply H2.
Col.
intro.
apply H2.
Col.
intro.
apply H2.
eapply (col_transitivity_1 _ C').
intro.
treat_equalities.
tauto.
Col.
apply bet_col in H16.
Col.
exists A.
split.
Col.
assumption.
assert(two_sides A B D' C').
eapply l9_8_2.
apply H21.
assumption.
assert(two_sides C' D' A B).
apply par_two_sides_two_sides.
apply parallel_comm.
apply parallel_symmetry.
assumption.
apply l9_2.
assumption.
apply l9_2 in H23.
apply invert_two_sides in H22.
assert(HH1:= l12_20 B D' A C' H18 H19 H22).
spliter.
assert(Cong_3 D' C A B A C').
repeat split; Cong.
apply cong3_conga in H27.
assert(one_side A C D D').
eapply one_side_transitivity.
eapply col_one_side.
Focus 3.
apply invert_one_side.
apply one_side_symmetry.
apply H0.
apply out_col in H.
Col.
assumption.
apply l12_6.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.
assert(out C D' D).
unfold inter in H8.
spliter.
induction H30.
apply l6_6.
apply bet_out.
intro.
treat_equalities.
unfold Par_strict in H1.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H12.
Col.
assumption.
induction H30.
apply bet_out.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
apply between_symmetry.
assumption.
assert(two_sides A C D D').
unfold two_sides.
repeat split.
auto.
unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H28.
tauto.
unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H31.
tauto.
exists C.
split.
Col.
apply between_symmetry.
assumption.
apply l9_9 in H31.
contradiction.
unfold out in H.
spliter.
induction H31.
assert(out C A C').
unfold out.
repeat split.
assumption.
intro.
subst C'.
apply between_identity in H16.
subst C.
assert(HX:=not_par_strict_id A B D').
apply HX.
contradiction.
left.
assumption.
assert(Conga D' C A D C P).
eapply l11_10.
apply conga_refl.
3: apply H29.
3:apply H32.
intro.
treat_equalities.
unfold out in H29.
tauto.
intro.
treat_equalities.
unfold two_sides in H22.
spliter.
apply H12.
Col.
apply out_trivial.
intro.
treat_equalities.
unfold out in H29.
tauto.
unfold out.
repeat split.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.
unfold out in H32.
spliter.
induction H34.
eapply (l5_1 _ A).
auto.
apply between_symmetry.
assumption.
assumption.
right.
eapply between_exchange4.
apply H34.
apply between_symmetry.
assumption.
assert(Conga B A P B A C').
eapply l11_10.
apply (conga_refl B A P).
intro.
treat_equalities.
apply H2.
Col.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.
apply out_trivial.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.
unfold out.
repeat split.
intro.
treat_equalities.
unfold out in H32.
tauto.
auto.
eapply (l5_2 C).
auto.
assumption.
apply between_symmetry.
assumption.
eapply conga_trans.
apply H34.
eapply conga_trans.
apply conga_sym.
apply H27.
assumption.
apply conga_comm.
assert(Conga D C A B A C').
eapply l11_10.
apply H27.
apply l6_6.
assumption.
apply out_trivial.
assumption.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.
eapply l11_13.
apply conga_comm.
apply conga_sym.
apply H32.
eapply outer_transitivity_between.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
assumption.
auto.
apply between_symmetry.
assumption.
auto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.
assumption.
spliter.
induction(eq_dec_points A C).
treat_equalities.
unfold out in H.
spliter.
assert(HH:= H0).
unfold one_side in HH.
ex_and HH T.
unfold two_sides in *.
spliter.
induction H4.
assert(two_sides P A B D).
unfold two_sides.
repeat split.
auto.
assumption.
assumption.
exists A.
split.
Col.
assumption.
apply l9_9 in H14.
contradiction.
induction H4.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
left.
assumption.
apply out_trivial.
auto.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
right.
apply between_symmetry.
assumption.
apply out_trivial.
auto.
unfold one_side in H0.
ex_and H0 T.
unfold two_sides in *.
spliter.
apply False_ind.
apply H7.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
assumption.
Col.
unfold out in H.
spliter.
induction H14; apply bet_col in H14; Col.
Qed.
Lemma l12_22_aux : forall A B C D P, Distincts P A C -> Bet P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.
prolong B A B' B A .
unfold Distincts in H.
spliter.
assert(Conga P A B C A B').
apply l11_14.
assumption.
repeat split; auto.
assumption.
repeat split.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.
assert(Conga D C A D C P).
eapply l11_10.
apply conga_refl.
3: apply out_trivial.
unfold Conga in H2.
tauto.
5:apply out_trivial.
auto.
unfold Conga in H2.
tauto.
apply between_symmetry in H0.
apply bet_out in H0.
assumption.
auto.
auto.
apply out_trivial.
unfold Conga in H2.
tauto.
auto.
assert(Par A B' C D).
eapply l12_21_b.
assert(~Col B P A).
unfold one_side in H1.
ex_and H1 T.
unfold two_sides in H1.
tauto.
assert(two_sides P A B B').
unfold two_sides.
repeat split.
auto.
assumption.
intro.
apply H9.
apply col_permutation_1.
eapply (col_transitivity_1 _ B').
intro.
treat_equalities.
unfold Conga in H2.
tauto.
apply bet_col in H3.
Col.
Col.
exists A.
split.
Col.
assumption.
apply l9_2.
eapply l9_8_2.
eapply col_two_sides.
3:apply invert_two_sides.
3: apply H10.
apply bet_col in H0.
Col.
assumption.
eapply col_one_side.
3: apply invert_one_side.
3: apply H1.
apply bet_col in H0.
Col.
assumption.
eapply conga_trans.
apply conga_sym.
apply conga_comm.
apply H7.
eapply conga_trans.
apply H2.
apply conga_sym.
assumption.
apply parallel_symmetry.
eapply par_col_par.
2: apply parallel_symmetry.
2:apply H9.
unfold Conga in H2.
spliter.
auto.
apply bet_col in H3.
Col.
Qed.
Lemma l12_22_b : forall A B C D P, out P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.
induction(eq_dec_points A C).
subst C.
unfold Par.
right.
repeat split.
unfold Conga in H1.
spliter.
auto.
unfold Conga in H1.
spliter.
auto.
Col.
apply conga_comm in H1.
apply l11_22_aux in H1.
induction H1.
apply out_col in H1.
Col.
apply l9_9 in H1.
contradiction.
unfold out in H.
spliter.
induction H4.
eapply l12_22_aux.
2:apply H4.
repeat split; auto.
assumption.
assumption.
apply parallel_symmetry.
eapply l12_22_aux.
2:apply H4.
repeat split; auto.
eapply (col_one_side _ A).
apply bet_col in H4.
Col.
auto.
apply one_side_symmetry.
assumption.
apply conga_sym.
assumption.
Qed.
Lemma l11_22 : forall A B C D P, out P A C -> one_side P A B D -> (Conga B A P D C P <-> Par A B C D).
intros.
split;
intro.
eapply (l12_22_b _ _ _ _ P); assumption.
apply l12_22_a; assumption.
Qed.
Lemma l12_23 : forall A B C, ~Col A B C -> exists B', exists C' , two_sides A C B B' /\ two_sides A B C C' /\
Bet B' A C' /\ Conga A B C B A C' /\ Conga A C B C A B'.
intros.
assert(exists B0, is_midpoint B0 A B) by (apply midpoint_existence).
assert(exists C0, is_midpoint C0 A C) by (apply midpoint_existence).
ex_and H0 B0.
ex_and H1 C0.
prolong B C0 B' B C0.
prolong C B0 C' C B0.
exists B'.
exists C'.
assert(two_sides A C B B').
eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H0.
intro.
apply H.
Col.
split.
assumption.
Cong.
assert(two_sides A B C C').
eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H2.
assumption.
split.
assumption.
Cong.
split.
assumption.
split.
assumption.
assert(Par A B' C B).
eapply l12_17.
intro.
treat_equalities.
assert(C0 = B0).
eapply l7_17.
2: apply H2.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
assert(Par A C' B C).
eapply l12_17.
intro.
treat_equalities.
assert(C0 = B0).
eapply l7_17.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H2.
split.
apply between_symmetry.
assumption.
Cong.
assert(Par A B' A C').
eapply par_trans.
apply H8.
apply parallel_symmetry.
apply parallel_right_comm.
assumption.
apply par_id in H10.
assert(one_side A C B0 C').
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_2.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
spliter.
ex_and H11 T.
apply between_identity in H12.
subst T.
contradiction.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
spliter.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
apply H7.
Col.
left.
assumption.
assert(one_side A C B0 B).
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_3.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
tauto.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
tauto.
unfold is_midpoint in H2.
spliter.
left.
assumption.
assert(one_side A C B C').
eapply one_side_transitivity.
2:apply H11;
intro.
apply one_side_symmetry.
assumption.
assert(two_sides A C B' C').
apply l9_2.
eapply l9_8_2.
apply H6.
assumption.
split.
unfold two_sides in H14.
spliter.
ex_and H17 T.
assert(A = T).
eapply (inter_unicity A C B' C').
Col.
Col.
Col.
apply bet_col in H18.
Col.
intro.
apply H15.
Col.
intro.
treat_equalities.
contradiction.
subst T.
assumption.
split.
apply l9_2 in H7.
assert(HH:= l12_21_a A C' B C H7 H9).
apply conga_comm.
apply conga_sym.
assumption.
apply parallel_symmetry in H8.
apply invert_two_sides in H6.
assert(HH:= l12_21_a C B A B' H6 H8).
apply conga_comm.
assumption.
Qed.
End T12.
Section T12.
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
| H:(le ?X1 ?X2 ?X3 ?X3) |- _ => apply le_zero in H; smart_subst X2
| H:(is_midpoint ?A ?A ?B) |- _ => apply is_midpoint_id in H; smart_subst A
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 coplanar := fun A B C D: Tpoint => True.
Definition Par_strict := fun A B C D =>
A<>B /\ C<>D /\ coplanar A B C D /\ ~ exists X, Col X A B /\ Col X C D.
Definition Par := fun A B C D =>
Par_strict A B C D \/ (A<>B /\ C<>D /\ Col A C D /\ Col B C D).
Lemma par_reflexivity : forall A B, A<>B -> Par A B A B.
Proof.
intros.
unfold Par.
unfold Par_strict.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
apply col_trivial_3.
Qed.
Lemma par_strict_irreflexivity : forall A B, ~ Par_strict A B A B.
Proof.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; apply col_trivial_1.
Qed.
Lemma par_strict_symmetry :forall A B C D, Par_strict A B C D -> Par_strict C D A B.
Proof.
unfold Par_strict.
intros.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; assumption.
Qed.
Lemma parallel_symmetry :forall A B C D, Par A B C D -> Par C D A B.
Proof.
unfold Par.
intros.
induction H.
left.
apply par_strict_symmetry.
assumption.
spliter.
right.
repeat split;try assumption.
eapply (col_transitivity_1 _ D).
assumption.
Col.
Col.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.
Qed.
Lemma parallel_left_comm : forall A B C D, Par A B C D -> Par B A C D.
unfold Par.
intros.
induction H.
left.
unfold Par_strict in *.
spliter.
repeat split.
auto.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; Col.
right.
spliter.
repeat split.
auto.
assumption.
Col.
Col.
Qed.
Lemma parallel_right_comm : forall A B C D, Par A B C D -> Par A B D C.
intros.
apply parallel_symmetry in H.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
Qed.
Lemma parallel_comm : forall A B C D, Par A B C D -> Par B A D C.
intros.
apply parallel_left_comm.
apply parallel_right_comm.
assumption.
Qed.
Lemma l12_6 : forall A B C D, Par_strict A B C D -> one_side A B C D.
intros.
unfold Par_strict in H.
spliter.
assert(HH:= not_two_sides_one_side A B C D H).
apply HH.
intro.
apply H2.
exists C.
split.
Col.
apply col_trivial_1.
intro.
apply H2.
exists D.
split.
Col.
apply col_trivial_3.
intro.
apply H2.
unfold two_sides in H3.
spliter.
ex_and H6 T.
exists T.
apply bet_col in H7.
split; Col.
Qed.
Lemma perp_perp_col : forall X Y Z A B, Perp X Y A B -> Perp X Z A B -> Col X Y Z.
intros.
induction(classic(Col A B X)).
induction(eq_dec_points X A).
subst A.
assert(X <> B).
apply perp_distinct in H.
spliter.
assumption.
apply perp_right_comm in H.
apply perp_perp_in in H.
apply perp_in_comm in H.
apply perp_in_per in H.
apply perp_right_comm in H0.
apply perp_perp_in in H0.
apply perp_in_comm in H0.
apply perp_in_per in H0.
apply col_permutation_2.
eapply (per_per_col).
apply H.
assumption.
assumption.
assert(Perp A X X Y ).
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.
assert(Perp A X X Z).
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.
apply col_permutation_2.
eapply (per_per_col _ _ A).
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.
assumption.
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.
assert(HH0:=H).
assert(HH1:=H0).
unfold Perp in H.
unfold Perp in H0.
ex_and H Y0.
ex_and H0 Z0.
assert(HH2:=H).
assert(HH3:=H2).
apply perp_in_col in H.
apply perp_in_col in H2.
spliter.
assert(Perp X Y0 A B).
eapply perp_col.
intro.
subst Y0.
contradiction.
apply HH0.
assumption.
assert(Perp X Z0 A B).
eapply perp_col.
intro.
subst Z0.
contradiction.
apply HH1.
assumption.
assert(Y0 = Z0).
eapply l8_18_unicity.
apply H1.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Z0.
eapply (col_transitivity_1 _ Y0).
intro.
subst Y0.
contradiction.
Col.
Col.
Qed.
Lemma perp_perp_col_col : forall X1 X2 Y1 Y2 A B, Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> Col X2 Y1 Y2.
intros.
assert(HH0:= H).
assert(HH1:= H0).
unfold Perp in HH0.
unfold Perp in HH1.
ex_and HH0 X0.
ex_and HH1 Y0.
induction(eq_dec_points X1 Y2).
subst Y2.
assert(Perp Y1 X1 A B).
eapply perp_col.
intro.
subst Y1.
apply perp_distinct in H0.
spliter.
absurde.
apply H0.
apply col_trivial_2.
apply col_permutation_1.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.
assert(Perp Y2 X1 A B).
eapply perp_col.
auto.
apply perp_left_comm.
apply H0.
Col.
assert(Perp X1 Y2 A B).
eapply perp_left_comm.
assumption.
induction(eq_dec_points X1 Y1).
subst Y1.
apply col_permutation_2.
eapply perp_perp_col.
apply H6.
assumption.
assert(Perp X1 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H5.
Col.
induction (eq_dec_points X2 Y1).
subst Y1.
apply col_trivial_1.
assert(Perp X2 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H.
apply col_permutation_2.
eapply perp_perp_col.
apply H8.
assumption.
induction (eq_dec_points X2 Y2).
subst Y2.
apply col_trivial_3.
assert(Perp Y2 X2 A B).
eapply perp_col.
auto.
apply H5.
apply col_permutation_2.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.
eapply perp_perp_col.
apply H10.
apply perp_left_comm.
assumption.
Qed.
Lemma l12_9 : forall A1 A2 B1 B2 C1 C2, coplanar A1 A2 B1 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 -> Par A1 A2 B1 B2.
Proof.
intros.
unfold Par.
unfold Par_strict.
assert(A1 <> A2 /\ C1 <> C2).
apply perp_distinct.
assumption.
assert(B1 <> B2 /\ C1 <> C2).
apply perp_distinct.
assumption.
spliter.
induction(classic(Col A1 B1 B2)).
right.
repeat split; try assumption.
eapply perp_perp_col_col.
apply H0.
apply H1.
assumption.
left.
repeat split.
assumption.
assumption.
intro.
ex_and H7 AB.
apply H6.
induction(eq_dec_points AB A1).
subst AB.
assumption.
assert(Perp A1 AB C1 C2).
eapply perp_col.
auto.
apply H0.
Col.
eapply perp_perp_col_col.
apply perp_left_comm.
apply H10.
assumption.
assumption.
Qed.
Lemma parallel_existence : forall A B P, A <> B -> exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.
Proof.
intros.
induction(classic(Col A B P)).
exists A.
exists B.
repeat split.
assumption.
apply par_reflexivity.
assumption.
Col.
assert(exists P', Col A B P' /\ Perp A B P P').
eapply l8_18_existence.
assumption.
ex_and H1 P'.
assert(P <> P').
intro.
subst P'.
contradiction.
induction(eq_dec_points P' A).
subst P'.
assert(exists Q, Per Q P A /\ Cong Q P A B /\ one_side A P Q B).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
Col.
ex_and H4 Q.
exists P.
exists Q.
assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.
repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.
apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.
assert(exists Q, Per Q P P' /\ Cong Q P A B /\ one_side P' P Q A).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
eapply (col_transitivity_1 _ P').
auto.
Col.
Col.
ex_and H5 Q.
exists P.
exists Q.
assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H6.
apply cong_identity in H6.
contradiction.
repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.
apply per_perp_in in H5.
apply perp_in_perp in H5.
induction H5.
apply perp_distinct in H5.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.
Qed.
Lemma par_not_col : forall A B C D X, Par_strict A B C D -> Col X A B -> ~Col X C D.
intros.
unfold Par_strict in H.
spliter.
intro.
apply H3.
exists X.
split; assumption.
Qed.
Lemma not_diff_eq : forall A B : Tpoint, ~ A <> B -> A = B.
intros.
induction(classic (A = B)).
assumption.
contradiction.
Qed.
Lemma not_not : forall P : Prop, ~~P -> P.
intros.
induction(classic P).
assumption.
contradiction.
Qed.
Lemma not_par_strict_inter_exists : forall A1 B1 A2 B2, ~Par_strict A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par_strict in H.
apply not_and in H.
induction H.
exists A2.
apply not_diff_eq in H.
subst B1.
split.
apply col_trivial_1.
apply col_trivial_3.
apply not_and in H.
induction H.
apply not_diff_eq in H.
subst B2.
exists A1.
split.
apply col_trivial_3.
apply col_trivial_1.
apply not_and in H.
induction H.
apply False_ind.
apply H.
unfold coplanar.
apply I.
apply not_not in H.
ex_and H X.
exists X.
split.
Col.
Col.
Qed.
Lemma not_par_inter_exists : forall A1 B1 A2 B2, ~Par A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par in H.
apply not_or in H.
spliter.
apply not_par_strict_inter_exists.
assumption.
Qed.
Lemma not_strict_par1 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
assert(exists X, Col X A B /\ Col X C D).
exists X.
split; Col.
contradiction.
spliter.
apply col_permutation_1.
eapply col_transitivity_1.
apply H2.
Col.
Col.
Qed.
Lemma not_strict_par2 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B D.
intros.
eapply not_strict_par1.
apply parallel_right_comm.
apply H.
apply H0.
Col.
Qed.
Lemma not_strict_par : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C /\ Col A B D.
intros.
split.
eapply not_strict_par1.
apply H.
apply H0.
assumption.
eapply not_strict_par2.
apply H.
apply H0.
assumption.
Qed.
Lemma not_par_not_col : forall A B C, A <> B -> A <> C -> ~Par A B A C -> ~Col A B C.
intros.
intro.
apply H1.
unfold Par.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
Col.
Qed.
Lemma not_par_inter_unicity : forall A B C D X Y, A <> B -> C <> D -> ~Par A B C D -> Col A B X -> Col C D X -> Col A B Y -> Col C D Y -> X = Y.
intros.
induction(eq_dec_points C Y).
subst Y.
induction (eq_dec_points C X).
subst X.
reflexivity.
eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
apply parallel_symmetry.
unfold Par.
right.
repeat split.
assumption.
assumption.
Col.
assert(Col A C X).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.
assert(Col A C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ X).
assumption.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ C).
intro.
subst C.
apply not_par_not_col in H1.
apply H1.
eapply (col_transitivity_1 _ _).
apply H6.
Col.
Col.
assumption.
assumption.
Col.
assumption.
assumption.
eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
unfold Par.
right.
repeat split; try assumption.
assert(Col A C Y).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.
assert(Col B C Y).
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.
assumption.
Qed.
Lemma not_par_two_sides : forall A B C D, A <> B -> C <> D -> ~Par A B C D -> exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y.
intros.
assert(HH:=H1).
apply not_par_inter_exists in H1.
ex_and H1 T.
induction(eq_dec_points C T).
subst T.
prolong D C Y D C.
exists D.
exists Y.
repeat split.
apply col_trivial_2.
apply bet_col in H3.
Col.
assumption.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
induction(eq_dec_points A C).
subst C.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
Col.
apply bet_col in H3.
Col.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
assert(Col Y A C).
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
assumption.
Col.
assert(Col A C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
apply bet_col in H3.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ _).
apply H5.
Col.
assumption.
exists C.
split; Col.
prolong C T Y C T.
exists C.
exists Y.
repeat split.
apply col_trivial_3.
eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col in H4.
assumption.
assumption.
intro.
assert(C=T).
eapply not_par_inter_unicity.
3:apply HH.
assumption.
assumption.
Col.
apply col_trivial_3.
assumption.
Col.
contradiction.
intro.
assert(Y= T).
eapply not_par_inter_unicity.
3: apply HH.
assumption.
assumption.
Col.
eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col.
assumption.
assumption.
Col.
subst Y.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.
exists T.
split.
Col.
assumption.
Qed.
Lemma not_par_other_side : forall A B C D P, A <> B -> C <> D -> ~Par A B C D -> ~Col A B P -> exists Q, Col C D Q /\ two_sides A B P Q.
intros.
assert(exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y).
apply not_par_two_sides.
assumption.
assumption.
assumption.
ex_and H3 X.
ex_and H4 Y.
induction(classic(two_sides A B P X)).
exists X.
split; assumption.
apply not_two_sides_one_side in H6.
exists Y.
split.
assumption.
eapply l9_8_2.
apply H5.
apply one_side_symmetry.
assumption.
assumption.
intro.
apply H2.
Col.
unfold two_sides in H5.
spliter.
assumption.
Qed.
Lemma inter_unicity_not_par : forall A B C D P, ~Col A B C -> Col A B P -> Col C D P -> ~Par A B C D.
intros.
intro.
unfold Par in H2.
induction H2.
unfold Par_strict in H2.
spliter.
apply H5.
exists P.
split; Col.
spliter.
apply H.
apply col_permutation_1.
eapply col_transitivity_1.
apply H3.
Col.
Col.
Qed.
Lemma par_strict_one_side : forall A B C D P, Par_strict A B C D -> Col C D P -> one_side A B C P.
Proof.
intros.
assert(HH:= H).
unfold Par_strict in HH.
spliter.
apply l12_6 in H.
unfold one_side in *.
ex_and H C'.
exists C'.
split.
assumption.
apply not_one_side_two_sides.
assumption.
intro.
apply H4.
exists P.
split; Col.
unfold two_sides in H.
spliter.
assumption.
intro.
apply H4.
unfold one_side in H6.
ex_and H6 P'.
assert(one_side A B P C').
eapply l9_8_1.
apply H6.
assumption.
assert(two_sides A B P C).
eapply l9_8_2.
apply l9_2.
apply H.
apply one_side_symmetry.
assumption.
unfold two_sides in H9.
spliter.
ex_and H12 T.
exists T.
split.
assumption.
induction(eq_dec_points C P).
subst P.
apply between_identity in H13.
subst T.
apply col_trivial_1.
eapply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
apply bet_col in H13.
Col.
Qed.
Lemma col_not_col_not_par : forall A B C D, (exists P, Col A B P /\ Col C D P) -> (exists Q, Col C D Q /\ ~Col A B Q) -> ~Par A B C D.
intros.
ex_and H P.
ex_and H0 Q.
intro.
unfold Par in H3.
induction H3.
unfold Par_strict in H3.
spliter.
apply H6.
exists P.
split; Col.
spliter.
apply H2.
eapply col3.
apply H4.
Col.
Col.
Col.
Qed.
Lemma par_distincts : forall A B C D, Par A B C D -> (Par A B C D /\ A <> B /\ C <> D).
intros.
split.
assumption.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
split; assumption.
spliter.
split; assumption.
Qed.
Lemma par_not_col_strict : forall A B C D P, Par A B C D -> Col C D P -> ~Col A B P -> Par_strict A B C D.
intros.
apply parallel_symmetry in H.
unfold Par in H.
induction H.
apply par_strict_symmetry.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H5 X.
apply H1.
assert(Col A C D).
eapply (col_transitivity_1 _ B).
assumption.
Col.
Col.
assert(Col B C D).
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.
Lemma par_strict_all_one_side : forall A B C D, Par_strict A B C D -> (forall P, Col C D P -> one_side A B C P).
intros.
eapply par_strict_one_side.
apply H.
assumption.
Qed.
Lemma all_one_side_par_strict : forall A B C D, C <> D -> (forall P, Col C D P -> one_side A B C P) -> Par_strict A B C D.
intros.
unfold Par_strict.
repeat split.
assert(HH:=H0 D (col_trivial_2 _ _)).
unfold one_side in HH.
ex_and HH C0.
unfold two_sides in H1.
spliter.
assumption.
assumption.
intro.
ex_and H1 X.
assert(HH:= H0 X (col_permutation_1 _ _ _ H2) ).
unfold one_side in HH.
ex_and HH M.
unfold two_sides in H4.
spliter.
contradiction.
Qed.
Lemma col_eq : forall A B X Y, A <> X -> Col A X Y -> Col B X Y -> ~Col A X B -> X = Y.
intros.
eapply inter_unicity.
apply col_trivial_2.
3: apply H0.
apply col_trivial_2.
apply H1.
intro.
apply H2.
Col.
assumption.
Qed.
Lemma par_col_par : forall A B C D D', C <> D' -> Par A B C D -> Col C D D' -> Par A B C D'.
intros.
unfold Par in *.
induction H0.
left.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H4.
ex_and H5 P.
exists P.
split.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
Col.
Col.
right.
spliter.
repeat split.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
Qed.
Lemma par_col2_par : forall A B C D E F, E <> F -> Par A B C D -> Col C D E -> Col C D F -> Par A B E F.
intros.
induction (eq_dec_points C E).
subst E.
eapply par_col_par.
assumption.
apply H0.
assumption.
eapply par_col_par.
assumption.
apply parallel_right_comm.
eapply par_col_par.
apply H3.
apply H0.
assumption.
apply col_permutation_2.
eapply col2.
apply par_distincts in H0.
spliter.
apply H5.
assumption.
assumption.
Qed.
Lemma par_strict_col2_par_strict : forall A B C D E F, E <> F -> Par_strict A B C D -> Col C D E -> Col C D F -> Par_strict A B E F.
intros.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H5.
ex_and H6 X.
exists X.
split.
assumption.
assert(Col C E F).
eapply col2.
apply H3.
assumption.
assumption.
assert(Col D E F).
eapply (col2 _ C).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.
Lemma parallel_unicity : forall A1 A2 B1 B2 C1 C2 P,
~ Col P A1 A2 ->
Par A1 A2 B1 B2 -> Col P B1 B2 ->
Par A1 A2 C1 C2 -> Col P C1 C2 ->
Col C1 B1 B2 /\ Col C2 B1 B2.
intros.
apply par_distincts in H0.
apply par_distincts in H2.
spliter.
assert(Par_strict A1 A2 B1 B2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
assert(Par_strict A1 A2 C1 C2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
induction(classic(Col C1 B1 B2 /\ Col C2 B1 B2)).
assumption.
apply not_and in H10.
assert(exists C', Col C1 C2 C' /\ two_sides B1 B2 A1 C').
apply not_par_other_side.
assumption.
assumption.
apply col_not_col_not_par.
exists P.
split; Col.
induction H10.
exists C1.
split.
apply col_trivial_3.
intro.
apply H10.
Col.
exists C2.
split.
apply col_trivial_2.
intro.
apply H10.
Col.
intro.
unfold Par_strict in H8.
spliter.
apply H14.
exists A1.
split.
apply col_trivial_1.
Col.
ex_and H11 C'.
assert(HH:=H12).
unfold two_sides in H12.
spliter.
ex_and H15 B.
double C' P C.
unfold is_midpoint in H17.
spliter.
assert(exists D, Bet B D C /\ Bet P D A1).
eapply inner_pasch.
apply H16.
apply between_symmetry.
assumption.
ex_and H19 D.
assert(C' <> P).
intro.
subst C'.
contradiction.
assert (Par A1 A2 C' P).
eapply par_col2_par.
assumption.
apply H2.
Col.
Col.
assert(Par_strict A1 A2 C' P).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
apply col_trivial_2.
intro.
apply H.
Col.
assert(B <> P).
intro.
subst B.
eapply (par_not_col _ _ _ _ A1) in H23.
apply H23.
apply bet_col in H16.
Col.
apply col_trivial_1.
assert(P <> C).
intro.
subst C.
apply cong_identity in H18.
subst C'.
absurde.
assert(Col B P B1).
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
assert(Col B P B2).
apply col_permutation_1.
eapply (col_transitivity_1 _ B1).
auto.
Col.
Col.
assert(Col C' P C1).
induction(eq_dec_points C' C1).
subst C1.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ ).
apply H5.
assumption.
Col.
assert(Col C P C1).
induction(eq_dec_points C' C1).
subst C1.
apply bet_col in H17.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.
assert(Col C' P C2).
induction(eq_dec_points C' C2).
subst C2.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
assert(Col C P C2).
induction(eq_dec_points C' C2).
subst C2.
apply bet_col in H17.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.
assert(~Col B P C).
intro.
assert(Col B P C').
apply col_permutation_2.
eapply col_transitivity_1.
apply H25.
apply bet_col in H17.
Col.
Col.
apply H14.
apply (col3 B P); assumption.
assert(P <> D).
intro.
subst D.
apply bet_col in H19.
contradiction.
assert(HE:=euclid P B C D A1 H20 H19 H33).
ex_and HE X.
ex_and H34 Y.
assert(Hx:= l12_6 A1 A2 P X).
induction(eq_dec_points P X).
subst X.
apply between_identity in H34.
subst B.
absurde.
assert(Par_strict A1 A2 P X).
eapply (par_strict_col2_par_strict _ _ B1 B2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply col3.
apply H24.
assumption.
assumption.
apply bet_col in H34.
Col.
apply Hx in H38.
assert(Hy:= l12_6 A1 A2 P Y).
induction(eq_dec_points P Y).
subst Y.
apply between_identity in H35.
subst C.
absurde.
assert(Par_strict A1 A2 P Y).
eapply (par_strict_col2_par_strict _ _ C1 C2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply (col3 C P).
auto.
assumption.
assumption.
apply bet_col in H35.
Col.
apply Hy in H40.
assert(one_side A1 A2 X Y).
eapply one_side_transitivity.
2:apply H40.
unfold one_side in H38.
unfold one_side.
ex_and H38 Z.
exists Z.
split.
assumption.
assumption.
assert(Ho:=H41).
unfold one_side in H41.
ex_and H41 Z.
unfold two_sides in H41.
unfold two_sides in H42.
spliter.
assert(two_sides A1 A2 X Y).
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists A1.
split.
apply col_trivial_1.
assumption.
apply l9_9 in H49.
contradiction.
Qed.
Lemma par_trans : forall A1 A2 B1 B2 C1 C2, Par A1 A2 B1 B2 -> Par B1 B2 C1 C2 -> Par A1 A2 C1 C2.
intros.
apply par_distincts in H.
apply par_distincts in H0.
spliter.
induction(classic(Par A1 A2 C1 C2)).
assumption.
apply not_par_inter_exists in H5.
ex_and H5 X.
induction(classic(Col X B1 B2)).
unfold Par in H, H0.
induction H.
eapply (par_not_col _ _ _ _ X) in H.
contradiction.
Col.
induction H0.
eapply (par_not_col _ _ _ _ X) in H0.
apply False_ind.
apply H0.
Col.
assumption.
spliter.
unfold Par.
right.
repeat split; try assumption.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
apply parallel_symmetry in H.
apply col_permutation_2 in H5.
apply col_permutation_2 in H6.
assert(HH:=parallel_unicity B1 B2 A1 A2 C1 C2 X H7 H H5 H0 H6).
spliter.
apply parallel_symmetry .
unfold Par.
right.
repeat split; try assumption.
Qed.
Definition inter A1 A2 B1 B2 X := (exists P, Col P B1 B2 /\ ~Col P A1 A2) /\ Col A1 A2 X /\ Col B1 B2 X.
Lemma inter_trivial : forall A B X, ~Col A B X -> inter A X B X X.
intros.
unfold inter.
split.
exists B.
split.
Col.
intro.
apply H.
Col.
split; Col.
Qed.
Lemma inter_sym : forall A B C D X, C <> D -> inter A B C D X -> inter C D A B X.
intros.
unfold inter in *.
spliter.
ex_and H0 P.
assert(A <> B).
intro.
subst B.
apply H3.
Col.
split.
induction(eq_dec_points A X).
treat_equalities.
exists B.
split.
Col.
intro.
apply H3.
eapply col3.
apply H.
Col.
Col.
Col.
exists A.
split.
Col.
intro.
apply H3.
assert(Col A P X).
eapply col3.
apply H.
Col.
Col.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H5.
Col.
Col.
split; assumption.
Qed.
Lemma inter_left_comm : forall A B C D X, inter A B C D X -> inter B A C D X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
assumption.
intro.
apply H2.
Col.
split; Col.
Qed.
Lemma inter_right_comm : forall A B C D X, inter A B C D X -> inter A B D C X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
Col.
assumption.
split; Col.
Qed.
Lemma inter_comm : forall A B C D X, inter A B C D X -> inter B A D C X.
intros.
apply inter_left_comm.
apply inter_right_comm.
assumption.
Qed.
Lemma l12_16 : forall A1 A2 B1 B2 C1 C2 X, Par A1 A2 B1 B2 -> inter A1 A2 C1 C2 X -> exists Y, inter B1 B2 C1 C2 Y.
intros.
assert(HH:= H).
unfold Par in H.
induction H.
unfold inter in H0.
spliter.
ex_and H0 P.
assert(~Col B1 B2 X).
intro.
unfold Par_strict in H.
spliter.
apply H7.
exists X.
auto with Col.
assert(HH1:= l8_18_existence B1 B2 X H4).
ex_and HH1 X0.
assert(~Par B1 B2 C1 C2).
intro.
assert(Par A1 A2 C1 C2).
eapply (par_trans _ _ B1 B2).
unfold Par.
left.
assumption.
assumption.
assert(~Par A1 A2 C1 C2).
apply col_not_col_not_par.
exists X.
auto with Col.
exists P.
auto with Col.
contradiction.
apply not_par_inter_exists in H7.
ex_and H7 Y.
exists Y.
split.
exists X.
split.
auto with Col.
intro.
apply H4.
auto with Col.
auto with Col.
unfold inter in H0.
spliter.
ex_and H0 P.
exists X.
split.
exists P.
split.
auto with Col.
intro.
apply H6.
eapply (col3 B1 B2); auto with Col.
split.
apply parallel_symmetry in HH.
unfold Par in HH.
induction HH.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists A1.
split.
auto with Col.
apply col_trivial_1.
spliter.
apply (col3 A1 A2); auto with Col.
auto with Col.
Qed.
Lemma l12_17 : forall A B C D P, A <> B -> is_midpoint P A C -> is_midpoint P B D -> Par A B C D.
intros.
induction(classic(Col A B P)).
unfold Par.
right.
induction(eq_dec_points A P).
subst P.
apply is_midpoint_id in H0.
subst C.
repeat split.
assumption.
intro.
treat_equalities.
apply l7_2 in H1.
apply is_midpoint_id in H1.
contradiction.
apply col_trivial_1.
unfold is_midpoint in H1.
spliter.
apply bet_col.
assumption.
induction(eq_dec_points B P).
subst P.
apply is_midpoint_id in H1.
subst D.
repeat split.
assumption.
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
auto.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0 .
Col.
apply col_trivial_3.
assert(HH0 := H0).
assert(HH1:= H1).
unfold is_midpoint in H0.
unfold is_midpoint in H1.
spliter.
apply bet_col in H1.
apply bet_col in H0.
assert(Col B C P).
eapply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
assert(Col B C D).
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.
repeat split.
assumption.
intro.
treat_equalities.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply HH0.
apply l7_2.
assumption.
contradiction.
induction(eq_dec_points A D).
subst D.
apply col_trivial_3.
assert(Col C D P).
eapply (col_transitivity_1 _ B).
intro.
subst C.
assert(A = D).
eapply midpoint_id.
eapply l7_2.
apply HH0.
assumption.
contradiction.
Col.
Col.
induction(eq_dec_points C P).
treat_equalities.
intuition.
apply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.
assumption.
assert(exists E, Col A B E /\ Perp A B P E).
eapply l8_18_existence.
assumption.
ex_and H3 E.
assert(A <> P).
intro.
treat_equalities.
apply H2.
apply col_trivial_3.
induction(eq_dec_points A E).
treat_equalities.
assert(Per P A B).
eapply perp_in_per.
apply perp_in_comm.
eapply perp_perp_in.
apply perp_sym.
apply perp_comm.
assumption.
prolong B A B' B A.
prolong B' P D' B' P.
assert(is_midpoint C D D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H0.
split.
apply H8.
Cong.
split.
assumption.
Cong.
assert(Per P A B').
eapply per_col.
apply H.
assumption.
apply bet_col in H6.
Col.
ex_and H3 B''.
assert(B' = B'').
eapply symmetric_point_unicity.
split.
apply H6.
Cong.
assumption.
subst B''.
assert(Cong P D P D').
apply (cong_transitivity _ _ B P).
unfold is_midpoint in H1.
spliter.
Cong.
apply (cong_transitivity _ _ B' P).
Cong.
Cong.
assert(Per P C D).
unfold Per.
exists D'.
split; assumption.
apply per_perp_in in H14.
apply perp_in_perp in H14.
induction H14.
apply perp_distinct in H14.
intuition.
eapply l12_9.
apply I.
apply H4.
apply perp_sym.
eapply perp_col.
auto.
apply H14.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0.
Col.
intro.
treat_equalities.
apply l7_2 in H0.
eapply is_midpoint_id in H0.
auto.
intro.
subst D.
assert(C = D').
apply is_midpoint_id.
assumption.
subst D'.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
prolong E P F E P.
assert(Col C D F).
eapply mid_preserves_col.
2: apply H0.
2:apply H1.
apply H3.
split.
assumption.
Cong.
prolong A E A' A E.
prolong A' P C' A' P.
assert(is_midpoint F C C').
eapply symmetry_preserves_midpoint.
apply H0.
split.
apply H7.
Cong.
split.
apply H12.
Cong.
split.
assumption.
Cong.
assert(Per P E A).
eapply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
Col.
assert(Cong P C P C').
eapply (cong_transitivity _ _ P A).
unfold is_midpoint in H0.
spliter.
Cong.
eapply (cong_transitivity _ _ P A').
unfold Per in H15.
ex_and H15 A''.
assert( A' = A'').
eapply symmetric_point_unicity.
split.
apply H10.
Cong.
assumption.
subst A''.
assumption.
Cong.
assert(Per P F C).
unfold Per.
exists C'.
split.
assumption.
assumption.
apply per_perp_in in H17.
apply perp_in_comm in H17.
apply perp_in_perp in H17.
induction H17.
eapply l12_9.
apply I.
apply H4.
eapply perp_col.
intro.
subst D.
assert (A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
treat_equalities.
apply perp_distinct in H17.
spliter.
auto.
apply perp_left_comm.
apply H17.
apply bet_col in H7.
Col.
Col.
apply perp_distinct in H17.
spliter.
tauto.
intro.
treat_equalities.
apply perp_distinct in H4.
spliter.
tauto.
intro.
subst C.
assert(F = C').
apply is_midpoint_id .
assumption.
treat_equalities.
assert(A = E).
eapply midpoint_id.
apply l7_2.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
tauto.
Qed.
Lemma l12_18_a : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par A B C D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
spliter.
eapply l12_17.
intro.
subst B.
apply H1.
apply col_trivial_1.
apply H5.
apply H6.
Qed.
Lemma l12_18_b : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par B C D A.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply l12_18_a.
assumption.
Cong.
intro.
apply H1.
assert(Col B C P).
eapply col_transitivity_1.
apply H2.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
apply H4.
Col.
Qed.
Lemma l12_18_c : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> two_sides B D A C.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
assert(Col A B P).
apply col_permutation_2.
eapply (col2 _ D).
assumption.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
apply H1.
assert(Col B P C).
eapply (col2 _ D).
assumption.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
exists P.
split.
Col.
spliter.
unfold is_midpoint in H5.
tauto.
Qed.
Lemma l12_18_d : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> two_sides A C B D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply (l12_18_c _ _ _ _ P).
Cong.
Cong.
intro.
apply H1.
assert(Col A B P).
eapply col_permutation_2.
eapply col2.
apply H2.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
contradiction.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
Qed.
Lemma l12_18 : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
B <> D -> Col A P C -> Col B P D
-> Par A B C D /\ Par B C D A /\
two_sides B D A C /\ two_sides A C B D.
intros.
split.
apply (l12_18_a _ _ _ _ P); assumption.
split.
apply (l12_18_b _ _ _ _ P); assumption.
split.
apply (l12_18_c _ _ _ _ P); assumption.
apply (l12_18_d _ _ _ _ P); assumption.
Qed.
Lemma l12_19 : forall A B C D , ~Col A B C -> Par A B C D -> Par B C D A ->
Cong A B C D /\ Cong B C D A /\
two_sides B D A C /\ two_sides A C B D.
intros.
assert(exists P, is_midpoint P A C) by (eapply midpoint_existence).
ex_and H2 P.
double B P D'.
assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.
assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_1.
apply H3.
assumption.
assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H0.
apply H6.
assert(Col C D D').
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists C.
split; apply col_trivial_1.
spliter.
Col.
assert(Par B C D' A).
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_2.
apply H2.
apply l7_2.
assumption.
assert(Par D A D' A).
eapply par_trans.
apply parallel_symmetry.
apply H1.
assumption.
assert(Col A D D').
unfold Par in H10.
induction H10.
unfold Par_strict in H10.
spliter.
apply False_ind.
apply H13.
exists A.
split; apply col_trivial_3.
spliter.
Col.
assert(D = D').
eapply inter_unicity.
3: apply H11.
apply col_trivial_2.
2: apply H8.
apply col_trivial_2.
intro.
apply H.
assert(Col P C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ A).
intro.
subst C.
apply H.
apply col_trivial_3.
Col.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.
assert(Col P C D').
apply col_permutation_2.
eapply (col2 _ D).
apply par_distincts in H0.
spliter.
assumption.
Col.
Col.
assert(Col P A D').
eapply (col2 _ C).
intro.
subst P.
apply l7_2 in H3.
apply is_midpoint_id in H3.
subst C.
apply H.
apply col_trivial_3.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.
assumption.
eapply (col3 P D').
intro.
subst D'.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P.
apply H.
unfold is_midpoint in H3.
spliter.
apply bet_col.
assumption.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply par_distincts in H0.
spliter.
assumption.
subst D'.
split.
Cong.
split.
Cong.
assert(B <> D).
intro.
subst D.
apply l7_3 in H2.
subst P.
apply H.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply False_ind.
apply H13.
exists B.
split; apply col_trivial_3.
spliter.
Col.
unfold is_midpoint in *.
spliter.
split.
eapply l12_18_c.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.
eapply l12_18_d.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.
Qed.
Lemma par_two_sides_two_sides : forall A B C D, Par A B C D -> two_sides B D A C -> two_sides A C B D.
intros.
apply par_distincts in H.
spliter.
unfold Par in H.
induction H.
Focus 2.
unfold two_sides in H0.
spliter.
apply False_ind.
apply H3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.
assert(A <> C).
intro.
subst C.
unfold Par_strict in H.
spliter.
apply H5.
exists A.
split; apply col_trivial_1.
unfold two_sides in *.
spliter.
ex_and H6 T.
repeat split.
assumption.
intro.
assert(Col T B C).
apply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
apply bet_col in H7.
Col.
Col.
apply H5.
apply col_permutation_2.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists C.
split.
Col.
apply col_trivial_1.
Col.
Col.
intro.
assert(Col T C D).
apply col_permutation_2.
apply (col_transitivity_1 _ A).
auto.
Col.
apply bet_col in H7.
Col.
apply H5.
apply col_permutation_1.
apply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists A.
split.
apply col_trivial_1.
Col.
Col.
Col.
exists T.
split.
apply bet_col in H7.
Col.
unfold Col in H6.
induction H6.
assert(HH:= outer_pasch C D T A B (between_symmetry _ _ _ H7) (between_symmetry _ _ _ H6)).
ex_and HH X.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.
induction H6.
assert(HH:= outer_pasch A B T C D H7 H6).
ex_and HH X.
apply False_ind.
unfold Par_strict in H.
spliter.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.
apply between_symmetry.
assumption.
Qed.
Lemma out_one_side : forall A B C D X, A <> B -> ~ Col A B C -> Col A B X -> out X C D -> one_side A B C D.
intros.
induction (eq_dec_points C D).
subst D.
apply one_side_reflexivity.
intro.
apply H0.
Col.
prolong C X C' C X.
exists C'.
assert(two_sides A B C C').
unfold two_sides.
repeat split.
assumption.
intro.
apply H0.
Col.
intro.
assert(C'=X).
eapply (inter_unicity A B C D).
Col.
apply out_col in H2.
eapply (col_transitivity_1 _ X).
intro.
treat_equalities.
contradiction.
Col.
apply bet_col in H4.
Col.
assumption.
apply out_col in H2.
Col.
intro.
apply H0.
Col.
assumption.
treat_equalities.
unfold out in H2.
tauto.
exists X.
split; Col.
assert(two_sides A B D C').
eapply (l9_5 _ _ _ _ X).
apply H6.
Col.
assumption.
split; assumption.
Qed.
Lemma l12_20_bis : forall A B C D, Par A B C D -> Cong A B C D -> two_sides B D A C ->
Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.
induction(eq_dec_points B C).
subst C.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_1.
induction(eq_dec_points A D).
subst D.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_3.
assert(~ Col A B C).
intro.
assert(Col A B D).
eapply not_strict_par1.
2: apply H4.
2: apply col_trivial_2.
apply parallel_right_comm.
assumption.
unfold two_sides in H1.
spliter.
contradiction.
assert(exists P, is_midpoint P A C) by (apply midpoint_existence).
ex_and H5 P.
double B P D'.
assert(Par B C D' A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.
assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H4.
apply col_trivial_1.
apply H6.
assumption.
assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.
assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H.
assumption.
assert(Col C D D').
unfold Par in H11.
induction H11.
unfold Par_strict in H11.
spliter.
apply False_ind.
apply H14.
exists C.
split; apply col_trivial_1.
spliter.
Col.
assert(Cong C D C D').
eapply (cong_transitivity _ _ A B).
Cong.
Cong.
assert(D = D' \/ is_midpoint C D D').
eapply l7_20.
Col.
assumption.
induction H14.
subst D'.
assert(Par B C D A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.
split.
assumption.
assert(HH:=l12_19 A B C D H4 H H14).
spliter.
split; assumption.
assert(two_sides A C B D).
apply par_two_sides_two_sides.
assumption.
assumption.
assert(HH:= H15).
assert(HH1:=H1).
unfold two_sides in H15, H1.
spliter.
ex_and H21 T.
ex_and H18 T'.
assert(T = T').
apply bet_col in H22.
apply bet_col in H23.
eapply (inter_unicity A C B D); Col.
subst T'.
assert(~Col B C T).
intro.
apply H16.
apply col_permutation_1.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
apply H20.
apply bet_col in H23.
Col.
Col.
Col.
assert(one_side B C T D).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_3.
apply bet_out in H23.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_3.
auto.
assert(one_side B C T A).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_2.
apply between_symmetry in H22.
apply bet_out in H22.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_2.
assumption.
assert(one_side B C A D).
apply (one_side_transitivity _ _ _ T).
apply one_side_symmetry.
assumption.
assumption.
assert(two_sides B C D D').
unfold two_sides.
repeat split.
assumption.
intro.
apply H20.
Col.
intro.
apply H20.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply H17.
apply col_trivial_3.
Col.
Col.
exists C.
split.
apply col_trivial_3.
unfold is_midpoint in H14.
spliter.
assumption.
assert(two_sides B C A D').
eapply l9_8_2.
apply H28.
apply one_side_symmetry.
assumption.
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H32.
unfold two_sides in H29.
spliter.
ex_and H35 X.
exists X.
split.
assumption.
apply bet_col in H36.
Col.
spliter.
apply False_ind.
apply H4.
eapply (col_transitivity_1 _ P).
intro.
subst P.
apply is_midpoint_id in H6.
tauto.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply l7_3 in H5.
subst P.
apply H4.
unfold is_midpoint in H6.
spliter.
auto.
apply bet_col.
assumption.
Col.
unfold is_midpoint in H5.
spliter.
apply bet_col in H5.
Col.
unfold is_midpoint in H6.
spliter.
apply bet_col in H6.
Col.
Qed.
Lemma l12_20 : forall A B C D, Par A B C D -> Cong A B C D -> two_sides A C B D ->
Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.
assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.
assert(HH:=l12_20_bis A B C D H H0 H2).
spliter.
split.
assumption.
split.
assumption.
assumption.
Qed.
Lemma par_one_or_two_sides : forall A B C D, Par_strict A B C D
-> two_sides A C B D /\ two_sides B D A C \/ one_side A C B D /\ one_side B D A C.
intros.
induction(classic (two_sides A C B D)).
left.
split.
assumption.
apply par_two_sides_two_sides.
apply parallel_comm.
unfold Par.
left.
assumption.
assumption.
right.
assert(HH:=H).
unfold Par_strict in H.
spliter.
assert(A <> C).
intro.
subst C.
apply H3.
exists A.
split; Col.
assert(B <> D).
intro.
subst D.
apply H3.
exists B.
split; Col.
split.
apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists C.
split; Col.
intro.
apply H3.
exists A.
split; Col.
assumption.
apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists D.
split; Col.
intro.
apply H3.
exists B.
split; Col.
intro.
apply H0.
apply par_two_sides_two_sides.
left.
assumption.
assumption.
Qed.
Lemma l12_21_a : forall A B C D, two_sides A C B D -> (Par A B C D -> Conga B A C D C A).
intros.
assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.
assert(B <> C).
intro.
subst B.
unfold two_sides in H.
spliter.
apply H2.
apply col_trivial_3.
assert(~Col B C D).
unfold two_sides in H1.
spliter.
intro.
apply H4.
Col.
assert(inter B C D C C).
repeat split.
exists D.
split.
apply col_trivial_1.
intro.
apply H3.
Col.
apply col_trivial_2.
apply col_trivial_2.
assert(HH:= parallel_existence B C A H2).
ex_and HH X.
ex_and H5 Y.
assert(HH:=l12_16 B C X Y D C C H6 H4).
ex_and HH D'.
apply par_distincts in H0.
spliter.
assert(~Col A B C).
intro.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.
exists C.
split; Col.
spliter.
contradiction.
assert(Par B C A D').
eapply par_col2_par.
intro.
subst D'.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.
unfold inter in H7.
ex_and H8 P.
exists A.
split; Col.
spliter.
contradiction.
apply H6.
Col.
unfold inter in H8.
spliter.
assumption.
assert(Par_strict A B C D).
unfold Par in H0.
induction H0.
assumption.
spliter.
apply False_ind.
apply H11.
apply col_permutation_1.
eapply (col2 _ D).
assumption.
Col.
Col.
assert(Par_strict B C A D').
unfold Par in H12.
induction H12.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H17 P.
apply H11.
eapply col2.
apply H14.
Col.
Col.
assert(Par A B C D').
eapply par_col_par.
intro.
subst D'.
unfold Par_strict in H14.
spliter.
apply H17.
exists C.
split; Col.
apply H0.
unfold inter in H8.
spliter.
Col.
apply parallel_right_comm in H12.
assert(HH:= l12_19 A B C D' H11 H15 H12).
spliter.
assert(A <> C).
unfold two_sides in H19.
spliter.
assumption.
assert(Conga B A C D' C A).
apply cong3_conga.
auto.
auto.
repeat split; Cong.
eapply l11_10.
apply H21.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold inter in H8.
spliter.
induction H23.
assert(one_side A C D D').
eapply l9_8_1.
apply l9_2.
apply H.
apply l9_2.
assumption.
assert(two_sides A C D D').
unfold two_sides.
repeat split.
assumption.
unfold two_sides in H.
spliter.
assumption.
unfold two_sides in H19.
spliter.
assumption.
exists C.
split.
apply col_trivial_3.
assumption.
apply l9_9 in H25.
contradiction.
induction H23.
apply bet_out in H23.
apply l6_6.
assumption.
intro.
treat_equalities.
auto.
auto.
apply between_symmetry in H23.
apply bet_out in H23.
assumption.
auto.
intro.
treat_equalities.
auto.
apply out_trivial.
auto.
Qed.
Lemma midpoint_preserves_out : forall A B C A' B' C' M, out A B C ->
is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
-> out A' B' C'.
intros.
unfold out in H.
spliter.
unfold out.
repeat split.
intro.
subst B'.
assert (A = B).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
intro.
subst C'.
assert (A = C).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
induction H4.
left.
apply (l7_15 A B C A' B' C' M); assumption.
right.
eapply (l7_15 A C B A' C' B' M); assumption.
Qed.
Lemma l12_21_b : forall A B C D, two_sides A C B D -> (Conga B A C D C A -> Par A B C D).
intros.
apply conga_diff in H0.
spliter.
assert(~Col A B C).
intro.
unfold two_sides in H.
spliter.
apply col_permutation_4 in H5.
assert(Col D C A).
eapply col_conga_col.
apply H5.
assumption.
contradiction.
assert(A <> B /\ C <> D).
auto.
spliter.
assert(HH:=segment_construction_3 C D A B H7 H6).
ex_and HH D'.
assert(Conga B A C D' C A).
eapply l11_10.
apply H0.
apply out_trivial.
assumption.
apply out_trivial.
assumption.
apply l6_6.
assumption.
apply out_trivial.
assumption.
assert(Cong D' A B C).
eapply cong2_conga_cong.
apply conga_sym.
apply H10.
Cong.
Cong.
assert(two_sides A C D' B).
eapply l9_5.
apply l9_2.
apply H.
apply col_trivial_3.
assumption.
unfold two_sides in H12.
spliter.
ex_and H15 M.
assert(B <> D').
intro.
treat_equalities.
contradiction.
assert(is_midpoint M A C /\ is_midpoint M B D').
apply l7_21.
assumption.
assumption.
Cong.
Cong.
Col.
apply bet_col in H16.
Col.
spliter.
assert(Par A B C D').
eapply l12_17.
assumption.
apply H18.
assumption.
eapply par_col_par.
auto.
apply H20.
apply out_col in H8.
Col.
Qed.
Lemma l12_21 : forall A B C D , two_sides A C B D -> (Conga B A C D C A <-> Par A B C D).
intros.
split.
intro.
apply l12_21_b ; assumption.
intro.
apply l12_21_a; assumption.
Qed.
Lemma par_id : forall A B C, Par A B A C -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H2.
exists A.
split; Col.
spliter.
Col.
Qed.
Lemma not_par_strict_id : forall A B C, ~ Par_strict A B A C.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; Col.
Qed.
Lemma l6_7_1 : forall A B C D, out A B C -> out A B D -> out A C D.
intros.
unfold out in *.
spliter.
repeat split.
assumption.
assumption.
induction H4; induction H2.
eapply l5_1.
2: apply H4.
auto.
assumption.
right.
eapply between_exchange4.
apply H2.
assumption.
left.
eapply between_exchange4.
apply H4.
assumption.
eapply l5_3.
apply H4.
apply H2.
Qed.
Lemma l12_22_a : forall A B C D P, out P A C -> one_side P A B D -> Par A B C D -> Conga B A P D C P.
intros.
unfold Par in H1.
induction H1.
assert(~Col A B C).
intro.
unfold Par_strict in H1.
spliter.
apply H5.
exists C.
split; Col.
assert( A <> C).
intro.
treat_equalities.
assert(HH := not_par_strict_id A B D).
contradiction.
assert(HH:= parallel_existence A C B H3).
ex_and HH X.
ex_and H4 Y.
assert(inter A C C D C).
apply inter_right_comm.
apply inter_trivial.
intro.
unfold Par_strict in H1.
spliter.
apply H10.
exists A.
split; Col.
assert(HH:= l12_16 A C X Y C D C H5 H7).
ex_and HH D'.
assert(Par A C B D').
eapply par_col2_par.
intro.
unfold Par_strict in H1.
spliter.
unfold inter in H8.
spliter.
treat_equalities.
apply H12.
exists B.
split; Col.
apply H5.
Col.
unfold inter in H8.
spliter.
assumption.
assert(Par A B C D').
eapply par_col_par.
intro.
treat_equalities.
apply H2.
apply parallel_comm in H9.
apply par_id in H9.
Col.
unfold Par.
left.
apply H1.
unfold inter in H8.
spliter.
assumption.
assert(Par_strict A C B D').
unfold Par in H9.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.
assert(Cong A B D' C /\
Cong B D' C A /\ two_sides B C A D' /\ two_sides A D' B C).
eapply l12_19.
eapply par_not_col.
apply H11.
Col.
apply parallel_right_comm.
assumption.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
spliter.
prolong C A C' C A.
assert(Par B D' A C').
eapply par_col_par.
intro.
treat_equalities.
tauto.
unfold Par.
left.
apply par_strict_symmetry.
apply H11.
apply bet_col in H16.
Col.
assert(Cong B D' A C').
eCong.
assert(Par_strict A B C D').
unfold Par in H10.
induction H10.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
tauto.
Col.
Col.
assert(HH := l12_6 A B C D' H20).
assert(two_sides A B C C').
unfold two_sides.
repeat split.
intro.
treat_equalities.
apply H2.
Col.
intro.
apply H2.
Col.
intro.
apply H2.
eapply (col_transitivity_1 _ C').
intro.
treat_equalities.
tauto.
Col.
apply bet_col in H16.
Col.
exists A.
split.
Col.
assumption.
assert(two_sides A B D' C').
eapply l9_8_2.
apply H21.
assumption.
assert(two_sides C' D' A B).
apply par_two_sides_two_sides.
apply parallel_comm.
apply parallel_symmetry.
assumption.
apply l9_2.
assumption.
apply l9_2 in H23.
apply invert_two_sides in H22.
assert(HH1:= l12_20 B D' A C' H18 H19 H22).
spliter.
assert(Cong_3 D' C A B A C').
repeat split; Cong.
apply cong3_conga in H27.
assert(one_side A C D D').
eapply one_side_transitivity.
eapply col_one_side.
Focus 3.
apply invert_one_side.
apply one_side_symmetry.
apply H0.
apply out_col in H.
Col.
assumption.
apply l12_6.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.
assert(out C D' D).
unfold inter in H8.
spliter.
induction H30.
apply l6_6.
apply bet_out.
intro.
treat_equalities.
unfold Par_strict in H1.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H12.
Col.
assumption.
induction H30.
apply bet_out.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
apply between_symmetry.
assumption.
assert(two_sides A C D D').
unfold two_sides.
repeat split.
auto.
unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H28.
tauto.
unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H31.
tauto.
exists C.
split.
Col.
apply between_symmetry.
assumption.
apply l9_9 in H31.
contradiction.
unfold out in H.
spliter.
induction H31.
assert(out C A C').
unfold out.
repeat split.
assumption.
intro.
subst C'.
apply between_identity in H16.
subst C.
assert(HX:=not_par_strict_id A B D').
apply HX.
contradiction.
left.
assumption.
assert(Conga D' C A D C P).
eapply l11_10.
apply conga_refl.
3: apply H29.
3:apply H32.
intro.
treat_equalities.
unfold out in H29.
tauto.
intro.
treat_equalities.
unfold two_sides in H22.
spliter.
apply H12.
Col.
apply out_trivial.
intro.
treat_equalities.
unfold out in H29.
tauto.
unfold out.
repeat split.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.
unfold out in H32.
spliter.
induction H34.
eapply (l5_1 _ A).
auto.
apply between_symmetry.
assumption.
assumption.
right.
eapply between_exchange4.
apply H34.
apply between_symmetry.
assumption.
assert(Conga B A P B A C').
eapply l11_10.
apply (conga_refl B A P).
intro.
treat_equalities.
apply H2.
Col.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.
apply out_trivial.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.
unfold out.
repeat split.
intro.
treat_equalities.
unfold out in H32.
tauto.
auto.
eapply (l5_2 C).
auto.
assumption.
apply between_symmetry.
assumption.
eapply conga_trans.
apply H34.
eapply conga_trans.
apply conga_sym.
apply H27.
assumption.
apply conga_comm.
assert(Conga D C A B A C').
eapply l11_10.
apply H27.
apply l6_6.
assumption.
apply out_trivial.
assumption.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.
eapply l11_13.
apply conga_comm.
apply conga_sym.
apply H32.
eapply outer_transitivity_between.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
assumption.
auto.
apply between_symmetry.
assumption.
auto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.
assumption.
spliter.
induction(eq_dec_points A C).
treat_equalities.
unfold out in H.
spliter.
assert(HH:= H0).
unfold one_side in HH.
ex_and HH T.
unfold two_sides in *.
spliter.
induction H4.
assert(two_sides P A B D).
unfold two_sides.
repeat split.
auto.
assumption.
assumption.
exists A.
split.
Col.
assumption.
apply l9_9 in H14.
contradiction.
induction H4.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
left.
assumption.
apply out_trivial.
auto.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
right.
apply between_symmetry.
assumption.
apply out_trivial.
auto.
unfold one_side in H0.
ex_and H0 T.
unfold two_sides in *.
spliter.
apply False_ind.
apply H7.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
assumption.
Col.
unfold out in H.
spliter.
induction H14; apply bet_col in H14; Col.
Qed.
Lemma l12_22_aux : forall A B C D P, Distincts P A C -> Bet P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.
prolong B A B' B A .
unfold Distincts in H.
spliter.
assert(Conga P A B C A B').
apply l11_14.
assumption.
repeat split; auto.
assumption.
repeat split.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.
assert(Conga D C A D C P).
eapply l11_10.
apply conga_refl.
3: apply out_trivial.
unfold Conga in H2.
tauto.
5:apply out_trivial.
auto.
unfold Conga in H2.
tauto.
apply between_symmetry in H0.
apply bet_out in H0.
assumption.
auto.
auto.
apply out_trivial.
unfold Conga in H2.
tauto.
auto.
assert(Par A B' C D).
eapply l12_21_b.
assert(~Col B P A).
unfold one_side in H1.
ex_and H1 T.
unfold two_sides in H1.
tauto.
assert(two_sides P A B B').
unfold two_sides.
repeat split.
auto.
assumption.
intro.
apply H9.
apply col_permutation_1.
eapply (col_transitivity_1 _ B').
intro.
treat_equalities.
unfold Conga in H2.
tauto.
apply bet_col in H3.
Col.
Col.
exists A.
split.
Col.
assumption.
apply l9_2.
eapply l9_8_2.
eapply col_two_sides.
3:apply invert_two_sides.
3: apply H10.
apply bet_col in H0.
Col.
assumption.
eapply col_one_side.
3: apply invert_one_side.
3: apply H1.
apply bet_col in H0.
Col.
assumption.
eapply conga_trans.
apply conga_sym.
apply conga_comm.
apply H7.
eapply conga_trans.
apply H2.
apply conga_sym.
assumption.
apply parallel_symmetry.
eapply par_col_par.
2: apply parallel_symmetry.
2:apply H9.
unfold Conga in H2.
spliter.
auto.
apply bet_col in H3.
Col.
Qed.
Lemma l12_22_b : forall A B C D P, out P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.
induction(eq_dec_points A C).
subst C.
unfold Par.
right.
repeat split.
unfold Conga in H1.
spliter.
auto.
unfold Conga in H1.
spliter.
auto.
Col.
apply conga_comm in H1.
apply l11_22_aux in H1.
induction H1.
apply out_col in H1.
Col.
apply l9_9 in H1.
contradiction.
unfold out in H.
spliter.
induction H4.
eapply l12_22_aux.
2:apply H4.
repeat split; auto.
assumption.
assumption.
apply parallel_symmetry.
eapply l12_22_aux.
2:apply H4.
repeat split; auto.
eapply (col_one_side _ A).
apply bet_col in H4.
Col.
auto.
apply one_side_symmetry.
assumption.
apply conga_sym.
assumption.
Qed.
Lemma l11_22 : forall A B C D P, out P A C -> one_side P A B D -> (Conga B A P D C P <-> Par A B C D).
intros.
split;
intro.
eapply (l12_22_b _ _ _ _ P); assumption.
apply l12_22_a; assumption.
Qed.
Lemma l12_23 : forall A B C, ~Col A B C -> exists B', exists C' , two_sides A C B B' /\ two_sides A B C C' /\
Bet B' A C' /\ Conga A B C B A C' /\ Conga A C B C A B'.
intros.
assert(exists B0, is_midpoint B0 A B) by (apply midpoint_existence).
assert(exists C0, is_midpoint C0 A C) by (apply midpoint_existence).
ex_and H0 B0.
ex_and H1 C0.
prolong B C0 B' B C0.
prolong C B0 C' C B0.
exists B'.
exists C'.
assert(two_sides A C B B').
eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H0.
intro.
apply H.
Col.
split.
assumption.
Cong.
assert(two_sides A B C C').
eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H2.
assumption.
split.
assumption.
Cong.
split.
assumption.
split.
assumption.
assert(Par A B' C B).
eapply l12_17.
intro.
treat_equalities.
assert(C0 = B0).
eapply l7_17.
2: apply H2.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
assert(Par A C' B C).
eapply l12_17.
intro.
treat_equalities.
assert(C0 = B0).
eapply l7_17.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H2.
split.
apply between_symmetry.
assumption.
Cong.
assert(Par A B' A C').
eapply par_trans.
apply H8.
apply parallel_symmetry.
apply parallel_right_comm.
assumption.
apply par_id in H10.
assert(one_side A C B0 C').
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_2.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
spliter.
ex_and H11 T.
apply between_identity in H12.
subst T.
contradiction.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
spliter.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
apply H7.
Col.
left.
assumption.
assert(one_side A C B0 B).
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_3.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
tauto.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
tauto.
unfold is_midpoint in H2.
spliter.
left.
assumption.
assert(one_side A C B C').
eapply one_side_transitivity.
2:apply H11;
intro.
apply one_side_symmetry.
assumption.
assert(two_sides A C B' C').
apply l9_2.
eapply l9_8_2.
apply H6.
assumption.
split.
unfold two_sides in H14.
spliter.
ex_and H17 T.
assert(A = T).
eapply (inter_unicity A C B' C').
Col.
Col.
Col.
apply bet_col in H18.
Col.
intro.
apply H15.
Col.
intro.
treat_equalities.
contradiction.
subst T.
assumption.
split.
apply l9_2 in H7.
assert(HH:= l12_21_a A C' B C H7 H9).
apply conga_comm.
apply conga_sym.
assumption.
apply parallel_symmetry in H8.
apply invert_two_sides in H6.
assert(HH:= l12_21_a C B A B' H6 H8).
apply conga_comm.
assumption.
Qed.
End T12.