Library Ch10_line_reflexivity_2D

Require Export Ch10_line_reflexivity.

Section T10.

Context `{MT:Tarski_2D}.
Context `{EqDec:EqDecidability Tpoint}.

Lemma image_cong_col : ∀ A B P P' X,
 P ≠ P' → is_image P P' A B → Cong P X P' X →
 Col A B X.
Proof.
intros.

unfold is_image in ×.
induction H0.
spliter.

unfold is_image_spec in H2.
spliter.

ex_and H2 M.
induction H3.

induction(eq_dec_points A M).
subst M.
assert (Perp P A A B).
eapply perp_col.
apply perp_distinct in H3.
spliter.
intro.
subst P.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P'.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H3.
unfold Col.
right; left.
apply midpoint_bet.
assumption.
apply perp_comm in H5.
apply perp_perp_in in H5.
apply perp_in_comm in H5.
apply perp_in_per in H5.

assert (Per X A P).
 unfold Per.
 ∃ P'.
 split.
 apply l7_2.
 assumption.

Cong.

apply l8_2 in H5.
apply col_permutation_2.
eapply per_per_col.
apply H5.
intro.
subst P.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P'.
absurde.
assumption.

assert (Perp P M M A).
eapply perp_col.
intro.
subst P.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P'.
absurde.
apply perp_sym.
apply perp_comm.
eapply perp_col.
assumption.
apply H3.
assumption.
unfold Col.
right; left.
apply midpoint_bet.
assumption.

apply perp_comm in H6.
apply perp_perp_in in H6.
apply perp_in_comm in H6.
apply perp_in_per in H6.

assert (Per X M P).
unfold Per.
∃ P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply l8_2 in H6.

assert (Col A X M).

eapply per_per_col.
apply H6.
intro.
subst P.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P'.
absurde.
assumption.
eapply col_transitivity_1.
apply H5.
apply col_permutation_5.
assumption.
apply col_permutation_5.
assumption.

subst P'.
absurde.

spliter;subst;Col.
Qed.

Lemma per_per_cong_1 :
 ∀ A B X Y, A ≠ B → Per A B X → Per A B Y →
 Cong B X B Y → X = Y ∨ is_midpoint B X Y.
Proof.
intros.
eapply l7_20.

apply col_permutation_5.
eapply per_per_col with A.
apply l8_2.
apply H0.
auto.
apply l8_2.
assumption.
assumption.
Qed.

Lemma per_per_cong : ∀ A B X Y,
 A ≠ B → Per A B X → Per A B Y → Cong B X B Y →
 X = Y ∨ is_image_spec X Y A B.
Proof.
intros.

assert (Col X Y B).
eapply per_per_col.
apply l8_2.
apply H0.
auto.
apply l8_2.
assumption.

induction (eq_dec_points X Y).
left.
assumption.
right.
unfold is_image_spec.
split.
∃ B.
split.
assert (X = Y ∨ is_midpoint B X Y).

eapply l7_20.
apply col_permutation_5.
assumption.
assumption.
induction H5.
contradiction.
apply l7_2.
assumption.
apply col_trivial_2.
left.

assert(Perp A B B Y).
eapply per_perp.
assumption.
intro.
subst Y.
apply cong_identity in H2.
subst X.
absurde.
assumption.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply perp_right_comm.
apply H5.
apply col_permutation_1.
assumption.
Qed.

Lemma per_per_cong_gen : ∀ A B X Y,
 A ≠ B → Per A B X → Per A B Y → Cong B X B Y →
 X = Y ∨ is_image X Y A B.
Proof.
intros.
assert (X = Y ∨ is_image_spec X Y A B)
 by (apply per_per_cong;auto).
induction H3.
tauto.
right.
unfold is_image.
tauto.
Qed.

End T10.