Library line_reflexivity
Require Export plane.
Section T10.
Context `{MT:Tarski}.
Ltac assert_cols :=
repeat
match goal with
| H:Bet ?X1 ?X2 ?X3 |- _ =>
not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
end.
Ltac clean_trivial_hyps :=
repeat
match goal with
| H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
| H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
| H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
| H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
| H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
| H:(Col ?X1 ?X1 ?X2) |- _ => clear H
| H:(Col ?X2 ?X1 ?X1) |- _ => clear H
| H:(Col ?X1 ?X2 ?X1) |- _ => clear H
end.
Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
match goal with
| H:(?X1 = ?X2) |- _ => smart_subst X2
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.
Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].
Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.
Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Ltac double A B A' :=
assert (mp:= mdp A B);
elim mp; intros A' ; intro; clear mp.
Definition is_image := fun P' P A B =>
(exists X, is_midpoint X P P' /\ Col A B X) /\ (Perp A B P P' \/ P=P').
Lemma ex_sym : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\ (exists M, Col A B M /\ is_midpoint M X Y).
intros.
induction (classic (Col A B X)).
exists X.
split.
right.
reflexivity.
exists X.
split.
assumption.
apply l7_3_2.
assert (exists M, Col A B M /\ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H0 M.
double X M Z.
exists Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
exists M.
split.
assumption.
assumption.
Qed.
Lemma ex_sym1 : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\ (exists M, Col A B M /\ is_midpoint M X Y /\ is_image X Y A B).
intros.
induction (classic (Col A B X)).
exists X.
split.
right.
reflexivity.
exists X.
split.
assumption.
split.
apply l7_3_2.
unfold is_image.
split.
exists X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
assert (exists M, Col A B M /\ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H0 M.
double X M Z.
exists Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
exists M.
split.
assumption.
split.
assumption.
unfold is_image.
split.
exists M.
split.
apply l7_2.
assumption.
assumption.
left.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst X.
apply l7_3 in H2.
subst Z.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
Qed.
Ltac ex_elim' H x := elim H; intros x ; clear H; intro H.
Ltac spliter1 :=
match goal with
| H:(?X1 /\ ?X2) |- _ => induction H
end.
Ltac ex_and' H x y := ex_elim H x y ; elim y.
Ltac symmetric X A B Y M :=
assert(Hsym := ex_sym1 A B X);
elim Hsym;
intro Y;
clear Hsym;
intro Hsym;
elim Hsym;
intro Hsym1;
intro Hsym2;
elim Hsym2;
intro M;
clear Hsym2;
intro Hsym2;
elim Hsym2;
clear Hsym2;
intro Hsym2;
intro Hsym3;
elim Hsym3;
clear Hsym3;
intro Hsym3;
intro Hsym4;
clear Hsym.
Lemma test : forall A B, (exists X, Col A B X) -> Col A A A.
intros.
ex_elim' H X.
apply col_trivial_1.
Qed.
Lemma l10_2_unicity : forall A B P P1 P2,
A<>B -> is_image P1 P A B -> is_image P2 P A B -> P1=P2.
intros.
unfold is_image in *.
spliter.
ex_and H0 X.
ex_and H1 Y.
induction H2; induction H3.
assert (P <> X).
intro.
subst X.
apply is_midpoint_id in H0.
subst P1.
apply perp_distinct in H3.
spliter.
absurde.
assert (P <> Y).
intro.
subst Y.
apply is_midpoint_id in H1.
subst P2.
apply perp_distinct in H2.
spliter.
absurde.
assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
induction (eq_dec_points X A).
subst X.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.
assert (Y = A).
eapply l8_18_unicity.
apply H10.
assumption.
apply perp_sym.
assumption.
apply col_trivial_3.
apply perp_sym.
assumption.
subst Y.
eapply symmetric_point_unicity.
apply H0.
apply H1.
assert (~ Col A B P /\ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
assert (Y = X).
eapply l8_18_unicity.
apply H11.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Y.
eapply symmetric_point_unicity.
apply H0.
apply H1.
subst P1.
assert (P <> Y).
intro.
subst Y.
apply l7_3 in H0.
subst X.
apply is_midpoint_id in H1.
subst P2.
eapply perp_distinct in H2.
spliter.
absurde.
assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l7_3 in H0.
subst X.
induction (eq_dec_points Y A).
subst Y.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto;
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
assert (~ Col A B P /\ Per P Y A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
subst P2.
assert (P <> X).
intro.
subst X.
apply l7_3 in H1.
subst Y.
apply is_midpoint_id in H0.
subst P1.
eapply perp_distinct in H3.
spliter.
absurde.
assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l7_3 in H1.
subst Y.
induction (eq_dec_points X A).
subst X.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
assert (~ Col A B P /\ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
subst P1.
subst P2.
reflexivity.
Qed.
Lemma l10_2_existence : forall A B P, exists P', is_image P' P A B.
intros.
induction (eq_dec_points A B).
subst B.
unfold is_image.
exists P.
split.
exists P.
split.
eapply l7_3_2.
apply col_trivial_1.
right.
reflexivity.
induction (classic (Col A B P)).
unfold is_image.
exists P.
split.
exists P.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
assert (exists X, Col A B X /\ Perp A B P X).
eapply l8_18_existence.
assumption.
ex_and H1 X.
double P X P'.
exists P'.
unfold is_image.
split.
exists X.
split; assumption.
left.
apply perp_sym.
eapply perp_col.
intro.
subst P'.
apply l7_3 in H3.
subst X.
apply perp_distinct in H2.
spliter.
absurde.
apply perp_sym.
apply H2.
unfold Col.
left.
apply mid_bet.
assumption.
Qed.
Lemma l10_4 : forall A B P P', is_image P P' A B -> is_image P' P A B.
intros.
unfold is_image in *.
spliter.
ex_and H X.
split.
exists X.
split.
apply l7_2.
assumption.
assumption.
induction H0.
left.
apply perp_right_comm.
assumption.
right.
subst P'.
reflexivity.
Qed.
Lemma l10_5 : forall A B P P' P'', A<>B -> is_image P' P A B -> is_image P'' P' A B -> P=P''.
Proof.
intros.
eapply l10_2_unicity.
apply H.
eapply l10_4.
apply H0.
assumption.
Qed.
Lemma l10_6_unicity : forall A B P P1 P2, A<>B -> is_image P P1 A B -> is_image P P2 A B -> P1 = P2.
intros.
eapply l10_2_unicity.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H1.
Qed.
Lemma l10_6_existence : forall A B P', A<>B -> exists P, is_image P' P A B.
intros.
assert (exists P, is_image P P' A B).
eapply l10_2_existence.
ex_and H0 P.
exists P.
apply l10_4.
assumption.
Qed.
Lemma l10_7 : forall A B P P' Q Q', A<>B -> is_image P' P A B -> is_image Q' Q A B -> P'=Q' -> P = Q.
intros.
subst Q'.
eapply l10_2_unicity.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H1.
Qed.
Lemma l10_8 : forall A B P, A<>B -> is_image P P A B -> Col P A B.
intros.
unfold is_image in H0.
spliter.
ex_and H0 X.
apply l7_3 in H0.
subst X.
apply col_permutation_2.
assumption.
Qed.
Lemma perp_col2 : forall A B C D X Y, Perp A B X Y -> C <> D -> Col A B C -> Col A B D -> Perp C D X Y.
intros.
assert(HH:=H).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points A C).
subst A.
eapply perp_col.
assumption.
apply H.
assumption.
assert(Perp A C X Y).
eapply perp_col.
assumption.
apply H.
assumption.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H6.
apply col_permutation_2;
eapply col2.
apply H3.
assumption.
assumption.
Qed.
Lemma image_col_cong : forall A B P P' X, is_image P P' A B -> Col A B X -> Cong P X P' X.
intros.
unfold is_image in H.
spliter.
ex_and H M.
induction H1.
assert (HH:= H1).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points M X).
subst X.
unfold is_midpoint in H.
spliter.
apply cong_symmetry.
apply cong_right_commutativity.
assumption.
assert (Perp M X P' P).
eapply perp_col2.
apply H1.
apply H5.
assumption.
assumption.
assert(~ Col A B P /\ Per P M X).
eapply l8_16_1.
assumption.
assumption.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
subst P.
apply l7_2 in H.
apply is_midpoint_id in H.
subst P'.
absurde.
apply perp_left_comm.
apply perp_sym.
apply H1;
eapply perp_left_comm.
unfold Col.
right; left.
apply mid_bet.
assumption.
spliter.
eapply l8_2 in H8.
unfold Per in H8.
ex_and H8 P0.
assert (P0 = P').
eapply symmetric_point_unicity.
apply H8.
apply l7_2.
assumption.
subst P0.
apply cong_commutativity.
assumption.
subst P'.
apply cong_reflexivity.
Qed.
Lemma perp_not_col : forall A B P, Perp A B P A -> ~ Col A B P.
intros.
assert (Perp_in A A B P A).
apply perp_perp_in.
assumption.
assert (Per P A B).
apply perp_in_per.
apply perp_in_sym.
assumption.
apply perp_in_left_comm in H0.
assert (~ Col B A P -> ~ Col A B P).
intro.
intro.
apply H2.
apply col_permutation_4.
assumption.
apply H2.
apply perp_distinct in H.
spliter.
apply per_not_col.
auto.
auto.
apply perp_in_per.
apply perp_in_right_comm.
assumption.
Qed.
Lemma osym_two_sides : forall P P' A B, P <> P' -> is_image P P' A B -> two_sides A B P P'.
intros.
unfold is_image in H0.
spliter.
ex_and H0 M.
induction H1.
Focus 2.
subst P'.
absurde.
assert (P <> M).
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
induction (eq_dec_points A M).
subst A.
assert (Perp M B P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.
apply perp_sym.
apply perp_right_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (Perp_in M M B P M).
eapply perp_perp_in.
assumption.
assert(Per B M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.
assert (B <> M).
intro.
repeat split.
subst B.
apply perp_distinct in H1.
spliter.
absurde.
assert (~Col B M P).
eapply per_not_col.
assumption.
auto.
assumption.
repeat split.
auto.
intro.
apply H8.
apply col_permutation_3.
assumption.
intro.
apply H8.
apply col_permutation_2.
eapply (col2 _ P').
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_4.
assumption.
exists M.
split.
apply col_trivial_1.
apply mid_bet.
apply l7_2.
assumption.
induction (eq_dec_points B M).
subst B.
assert (Perp M A P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.
apply perp_sym.
apply perp_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (Perp_in M M A P M).
eapply perp_perp_in.
assumption.
assert(Per A M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.
repeat split.
assumption.
assert (~Col A M P).
eapply per_not_col.
assumption.
auto.
assumption.
intro.
apply H8.
apply col_permutation_1.
assumption.
intro.
assert (Col M A P).
eapply (col_transitivity_1 _ P').
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
apply col_permutation_2.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
eapply (per_not_col ).
3: apply H7.
assumption.
auto.
apply col_permutation_4.
assumption.
exists M.
split.
apply col_trivial_3.
apply mid_bet.
apply l7_2.
assumption.
repeat split.
apply perp_distinct in H1.
spliter.
assumption.
assert(Perp P M A B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_right_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (~ Col M P A).
apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H6.
assumption.
intro.
apply H7.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H1.
spliter.
apply H1.
assumption.
apply col_permutation_1.
assumption.
assert(Perp P' M A B).
eapply perp_col.
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col M P' A).
apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H6.
assumption.
intro.
apply H7.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H1.
spliter.
apply H1.
assumption.
apply col_permutation_1.
assumption.
exists M.
split.
apply col_permutation_2.
assumption.
apply mid_bet.
apply l7_2.
assumption.
Qed.
Lemma image_id : forall A B T T', Col A B T -> is_image T T' A B -> T = T'.
intros.
unfold is_image in H0.
spliter.
ex_and H0 X.
induction H1.
assert (A <> B /\ T' <> T).
apply perp_distinct in H1.
spliter.
split;
assumption.
spliter.
Focus 2.
subst T'.
reflexivity.
induction (eq_dec_points A X).
subst X.
assert (Perp A B T' A).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst A.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col A T' B).
apply perp_not_col.
apply perp_comm.
apply perp_sym.
assumption.
assert (A = T).
eapply inter_unicity.
5: apply H6.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
assumption.
apply col_trivial_2.
assumption.
subst A.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
induction (eq_dec_points B X).
subst X.
assert (Perp A B T' B).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst B.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col B T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
assumption.
assert (B = T).
eapply inter_unicity.
5: apply H7.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst B.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
assert (Col A X T).
eapply col_transitivity_1.
apply H3.
assumption.
assumption.
assert (Perp A B T' X).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst X.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col X T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
eapply perp_col.
assumption.
apply H8.
assumption.
assert (X = T).
eapply inter_unicity.
5: apply H9.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst X.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
Qed.
Lemma osym_not_col : forall A B P P', is_image P P' A B -> ~ Col A B P -> ~ Col A B P'.
intros.
assert ( HH:= H).
unfold is_image in HH.
spliter.
ex_and H1 T.
intro.
induction H2.
assert (P'=P).
eapply image_id.
apply H4.
apply l10_4.
assumption.
subst P'.
apply perp_distinct in H2.
spliter.
absurde.
apply H0.
subst P'.
assumption.
Qed.
Lemma cong_cong_half : forall A M B A' M' B', is_midpoint M A B -> is_midpoint M' A' B' -> Cong A B A' B' -> Cong A M A' M'.
intros.
unfold is_midpoint in *.
spliter.
assert(exists M'', Bet A' M'' B' /\ Cong_3 A M B A' M'' B').
eapply l4_5.
assumption.
assumption.
ex_and H4 M''.
assert (is_midpoint M'' A' B').
unfold is_midpoint.
split.
assumption.
unfold Cong_3 in H5.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
eapply cong_transitivity.
apply H3.
assumption.
assert(M'=M'').
eapply l7_17;
unfold is_midpoint;
split.
apply H0.
apply H2.
apply H4.
unfold is_midpoint in H6.
spliter.
assumption.
subst M''.
unfold Cong_3 in H5.
spliter.
assumption.
Qed.
Lemma image_cong_col : forall A B P P' X, P <> P' -> is_image P P' A B -> Cong P X P' X -> Col A B X.
intros.
unfold is_image in H0.
spliter.
ex_and H0 M.
induction H2.
Focus 2.
subst P'.
absurde.
induction(eq_dec_points A M).
subst M.
assert (Perp P A A B).
eapply perp_col.
apply perp_distinct in H2.
spliter.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H2.
unfold Col.
right; left.
apply mid_bet.
assumption.
apply perp_comm in H4.
apply perp_perp_in in H4.
apply perp_in_comm in H4.
apply perp_in_per in H4.
assert (Per X A P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply l8_2 in H4.
apply col_permutation_2.
eapply per_per_col.
apply H4.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
assumption.
assert (Perp P M M A).
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
apply perp_sym.
apply perp_comm.
eapply perp_col.
assumption.
apply H2.
assumption.
unfold Col.
right; left.
apply mid_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 M P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply l8_2 in H5.
assert (Col A X M).
eapply per_per_col.
apply H5.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
assumption.
eapply col_transitivity_1.
apply H4.
apply col_permutation_5.
assumption.
apply col_permutation_5.
assumption.
Qed.
Lemma midpoint_preserves_image : forall A B P P' Q Q' M, A <> B -> Col A B M ->is_image P P' A B
-> is_midpoint M P Q -> is_midpoint M P' Q' -> is_image Q Q' A B.
intros.
assert (HH1:=H1).
unfold is_image in H1.
spliter.
ex_and H1 X.
induction H4.
double X M Y.
assert (is_midpoint Y Q Q').
eapply symmetry_preserves_midpoint.
apply H2.
apply H6.
apply H3.
apply l7_2.
apply H1.
assert (P <> P').
intro.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.
assert (Q <> Q').
intro.
subst Q'.
apply l7_3 in H7.
subst Q.
assert (P=P').
eapply l7_9.
apply H2.
apply H3.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.
split.
exists Y.
split.
apply l7_2.
apply H7.
induction (eq_dec_points X Y).
subst Y.
assumption.
eapply (colx _ _ M X).
assumption.
intro.
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
assumption.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
left.
assert(Per M Y Q).
unfold Per.
exists Q'.
split.
assumption.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H14.
apply cong_symmetry.
eapply cong_transitivity.
apply cong_symmetry.
apply H13.
eapply image_col_cong.
apply l10_4.
apply HH1.
assumption.
induction (eq_dec_points X Y).
subst Y.
apply l7_3 in H6.
subst X.
apply perp_sym.
eapply perp_col.
auto.
apply perp_left_comm.
eapply perp_col.
2:apply perp_sym.
2:apply H4.
intro.
subst Q'.
apply l7_3 in H3.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
eapply (col_transitivity_2 M).
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
eapply (col_transitivity_2 M).
intro.
subst Q'.
apply l7_2 in H7.
apply is_midpoint_id in H7.
subst Q.
absurde.
unfold Col.
right; right.
apply mid_bet.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
apply per_perp_in in H10.
apply perp_in_perp in H10.
induction H10.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_comm.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_comm.
eapply (perp_col Y Q).
intro.
subst Q.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_sym.
induction (eq_dec_points A M).
subst A.
apply perp_left_comm.
eapply (perp_col _ M).
auto.
apply perp_left_comm.
eapply (perp_col _ Y).
assumption.
assumption.
induction (eq_dec_points M X).
subst X.
apply is_midpoint_id in H6.
subst M.
apply col_trivial_1.
eapply (col2 _ X).
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_5.
assumption.
apply col_trivial_2.
induction (eq_dec_points B M).
subst M.
apply perp_left_comm.
apply (perp_col _ Y).
auto.
assumption.
induction (eq_dec_points B X).
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
eapply col_transitivity_1.
apply H13.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_1.
assumption.
eapply perp_col.
assumption.
apply perp_left_comm.
eapply (perp_col M Y).
auto.
assumption.
assert(Col B X M).
eapply col_transitivity_2.
apply H.
assumption.
assumption.
induction (eq_dec_points M X).
subst X.
apply is_midpoint_id in H6.
contradiction.
assert(Col B Y M).
apply col_permutation_1.
eapply (col_transitivity_2 X).
auto.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (col_transitivity_1 _ B).
auto.
apply col_permutation_2.
assumption.
apply col_permutation_3.
apply H0.
apply col_permutation_5.
apply H0.
apply col_trivial_2.
unfold Col.
left.
apply mid_bet.
apply H7.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
intro.
subst Q.
apply is_midpoint_id in H7.
subst Q'.
absurde.
subst P'.
apply l7_3 in H1.
subst P.
assert(Q = Q').
eapply l7_9.
apply l7_2.
apply H2.
apply l7_2.
apply H3.
subst Q'.
split.
exists Q.
split.
apply l7_3_2.
induction (eq_dec_points M X).
subst X.
assert(M=Q).
apply is_midpoint_id.
assumption.
subst Q.
assumption.
eapply colx.
assumption.
apply H1.
intro.
subst Q.
apply l7_3 in H2.
contradiction.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
apply H3.
right.
reflexivity.
Qed.
Definition is_image_in := fun M P' P A B =>
(is_midpoint M P P' /\ Col A B M) /\ (Perp A B P P' \/ P=P').
Lemma image_in_is_image : forall M A B P P' , is_image_in M P P' A B -> is_image P P' A B.
intros.
unfold is_image_in in H.
spliter.
unfold is_image.
split.
exists M.
split;
assumption.
assumption.
Qed.
Lemma image_image_in : forall A B P P' M, P <> P'-> is_image P P' A B -> Col A B M -> Col P M P' -> is_image_in M P P' A B.
intros.
unfold is_image_in.
split.
split.
assert(HH:=H0).
unfold is_image in H0.
spliter.
ex_and H0 M'.
induction H3.
assert (Perp P M' A B).
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H3.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (M'=M).
eapply inter_unicity.
apply H4.
unfold Col.
right; left.
apply mid_bet.
apply H0.
assumption.
apply col_permutation_5.
assumption.
induction (eq_dec_points A M').
subst M'.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
apply col_trivial_3.
apply col_trivial_2.
apply perp_distinct in H3.
spliter.
auto.
apply perp_sym.
assumption.
spliter.
intro.
apply H6.
apply col_permutation_5.
assumption.
assert (~ Col A B P /\ Per P M' A).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
assumption.
apply col_trivial_3.
assumption.
apply perp_sym.
assumption.
spliter.
intro.
apply H7.
apply col_permutation_5.
assumption.
apply perp_distinct in H3.
spliter.
auto.
subst M'.
assumption.
subst P'.
absurde.
assumption.
assert (HH:=H0).
unfold is_image in H0.
spliter.
induction H3.
left.
assumption.
right.
assumption.
Qed.
Lemma image_in_col : forall A B P P' Q Q' M, is_image_in M P P' A B -> is_image_in M Q Q' A B -> Col M P Q.
intros.
assert(is_image P P' A B).
eapply (image_in_is_image M).
assumption.
assert(is_image Q Q' A B).
eapply (image_in_is_image M).
assumption.
unfold is_image_in in *.
spliter.
induction H3.
induction H5.
induction (eq_dec_points A M).
subst M.
assert (Per B A P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H1.
apply col_trivial_2.
assert (Per B A Q).
unfold Per.
exists Q'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H2.
apply col_trivial_2.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H7.
apply perp_distinct in H3.
spliter.
assumption.
apply l8_2.
assumption.
assert (Per A M P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H1.
apply col_trivial_3.
assert (Per A M Q).
unfold Per.
exists Q'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H2.
apply col_trivial_3.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H8.
auto.
apply l8_2.
assumption.
subst P'.
apply l7_3 in H.
subst P.
apply col_trivial_1.
subst Q'.
apply l7_3 in H0.
subst Q.
apply col_trivial_3.
Qed.
Lemma image_in_col0 : forall A B P P' Y : Tpoint, is_image_in Y P P' A B -> Col P P' Y.
intros.
apply col_permutation_1.
eapply (image_in_col A B P P').
assumption.
assert (HH:=H).
apply image_in_is_image in H.
unfold is_image_in in HH.
spliter.
induction H1.
apply l10_4 in H.
eapply (image_image_in _ _ _ P ).
apply perp_distinct in H1.
spliter.
assumption.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
subst P'.
apply l7_3 in H0.
subst P.
unfold is_image_in.
repeat split.
apply between_trivial2.
apply cong_trivial_identity.
assumption.
right.
reflexivity.
Qed.
Lemma l10_10 : forall A B P Q P' Q', A<>B -> is_image P' P A B -> is_image Q' Q A B -> Cong P Q P' Q'.
intros.
intros.
assert(HH0 := H0).
assert(HH1 := H1 ).
unfold is_image in H0.
unfold is_image in H1.
spliter.
ex_and H0 X.
ex_and H1 Y.
assert (exists M, is_midpoint M X Y).
apply midpoint_existence.
ex_elim H6 M.
double P M P''.
double Q M Q''.
double P' M P'''.
apply cong_commutativity.
induction H3.
Focus 2.
subst P'.
apply l7_3 in H0.
subst P.
eapply image_col_cong.
apply l10_4.
apply HH1.
assumption.
induction H2.
Focus 2.
subst Q'.
apply l7_3 in H1.
subst Q.
apply cong_commutativity.
eapply image_col_cong.
apply l10_4.
apply HH0.
assumption.
assert (is_image P'' P''' A B).
eapply (midpoint_preserves_image _ _ _ _ _ _ M).
assumption.
induction (eq_dec_points X Y).
subst Y.
apply l7_3 in H7.
subst X.
assumption.
assert(Col A X Y).
eapply col_transitivity_1.
apply H.
assumption.
assumption.
assert(Col B X Y).
eapply (col_transitivity_1 _ A).
auto.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
eapply col_col.
apply H10.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l10_4.
apply HH0.
assumption.
assumption.
assert(P'' <> P''').
intro.
subst P'''.
assert( P' = P).
eapply l7_9.
apply H9.
assumption.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
assert (is_midpoint Y P'' P''').
eapply symmetry_preserves_midpoint.
apply H6.
apply H7.
apply H9.
assumption.
assert (Cong P'' Y P''' Y).
unfold is_midpoint in H12.
spliter.
apply cong_right_commutativity.
assumption.
assert (Cong Q Y Q' Y).
unfold is_midpoint in H1.
spliter.
apply cong_right_commutativity.
assumption.
assert (Col P'' Y Q).
apply col_permutation_2.
eapply image_in_col.
eapply image_image_in.
apply perp_distinct in H2.
spliter.
apply H15.
apply l10_4.
apply HH1.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (image_image_in _ _ _ P''').
assumption.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (l4_16 P'' Y Q P P''' Y Q' P').
repeat split.
assumption.
assumption.
unfold Col in H15.
induction H15.
assert(Bet P''' Y Q').
eapply (l7_15).
apply H12.
apply l7_3_2.
apply H1.
assumption.
eapply l2_l1.
apply H15.
apply H16.
assumption.
apply cong_commutativity.
assumption.
induction H15.
assert (Bet Y Q' P''').
eapply (l7_15).
apply l7_3_2.
apply H1.
apply H12.
assumption.
eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.
apply between_symmetry in H15.
assert (Bet Y P''' Q').
eapply (l7_15).
apply l7_3_2.
apply H12.
apply H1.
assumption.
apply cong_commutativity.
eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.
apply cong_commutativity.
assumption.
assert (Cong P Y P' Y).
eapply image_col_cong.
eapply l10_4.
apply HH0.
assumption.
assert (Cong P P'' P' P''').
induction(eq_dec_points X Y).
subst Y.
eapply l2_l1.
apply mid_bet.
apply H6.
apply H9.
apply l7_3 in H7.
subst X.
assumption.
apply l7_3 in H7.
subst X.
eapply cong_transitivity.
unfold is_midpoint in H6.
spliter.
apply cong_symmetry.
apply H7.
eapply cong_transitivity.
apply H16.
unfold is_midpoint in H9.
spliter.
assumption.
eapply l2_l1.
apply H6.
apply H9.
eapply image_col_cong.
apply l10_4.
apply HH0.
unfold is_midpoint in H7.
spliter.
eapply colx.
assumption.
3:apply H4.
3:apply H5.
auto.
intro.
subst X.
apply cong_symmetry in H18.
apply cong_identity in H18.
subst Y.
absurde.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H10.
eapply colx.
4:apply H4.
4:apply H5.
assumption.
auto.
intro.
subst X.
apply is_midpoint_id in H7.
contradiction.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply l10_4.
apply HH0.
assumption.
intro.
subst P''.
apply cong_symmetry in H13.
apply cong_identity in H13.
subst P'''.
absurde.
Qed.
Lemma per_per_cong' : forall 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.
intros.
eapply l7_20.
apply col_permutation_5.
eapply per_per_col.
apply l8_2.
apply H0.
auto.
apply l8_2.
assumption.
assumption.
Qed.
Lemma per_per_cong : forall 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.
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.
split.
exists 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 is_image_rev : forall P P' A B, is_image P P' A B -> is_image P P' B A.
unfold is_image.
intros.
spliter.
split.
ex_and H M.
exists M.
split.
assumption.
apply col_permutation_4.
assumption.
induction H0.
left.
apply perp_left_comm.
assumption.
right.
assumption.
Qed.
Lemma per_double_cong : forall A B C C', Per A B C -> is_midpoint B C C' -> Cong A C A C'.
intros.
unfold Per in H.
ex_and H C''.
assert (C' = C'').
eapply l7_9.
apply l7_2.
apply H0.
apply l7_2.
assumption.
subst C''.
assumption.
Qed.
Lemma midpoint_preserves_per : forall A B C A1 B1 C1 M, Per A B C ->
is_midpoint M A A1 -> is_midpoint M B B1 -> is_midpoint M C C1
-> Per A1 B1 C1.
intros.
unfold Per in *.
ex_and H C'.
double C' M C1'.
exists C1'.
split.
eapply symmetry_preserves_midpoint.
apply H2.
apply H1.
apply H4.
assumption.
eapply l7_16.
apply H0.
apply H2.
apply H0.
apply H4.
assumption.
Qed.
Lemma image_preserves_bet : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> Bet A B C -> Bet A' B' C'.
intros.
eapply l4_6.
apply H3.
unfold Cong_3.
repeat split;
eapply l10_10.
apply H.
apply l10_4;
assumption.
apply l10_4;
assumption.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
Qed.
Lemma image_preserves_midpoint : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> is_midpoint A B C -> is_midpoint A' B' C'.
intros.
unfold is_midpoint in *.
spliter.
repeat split.
eapply image_preserves_bet.
apply H.
apply H1.
apply H0.
apply H2.
assumption.
eapply cong_transitivity.
eapply l10_10.
apply H.
apply H1.
apply H0.
eapply cong_transitivity.
apply H4.
eapply l10_10.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H2.
Qed.
Lemma image_preserves_per : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> Per A B C -> Per A' B' C'.
intros.
double C B C1.
assert (exists C1', is_image C1 C1' X Y).
apply l10_6_existence.
assumption.
ex_and H5 C1'.
unfold Per.
exists C1'.
split.
eapply image_preserves_midpoint.
apply H.
apply H1.
apply H2.
apply H6.
assumption.
eapply cong_transitivity.
eapply l10_10.
apply H.
apply H0.
apply H2.
eapply cong_transitivity.
unfold Per in H3.
ex_and H3 C2.
assert (C2=C1).
eapply symmetric_point_unicity.
apply H3.
assumption.
subst C2.
apply H5.
eapply l10_10.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
Qed.
Lemma per_perp : forall A B C D, A <> B -> B <> C -> D <> B -> D <> C -> Col B C D -> Per A B C -> Perp C D A B.
intros.
apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
eapply (perp_col _ B).
auto.
apply perp_sym.
apply perp_right_comm.
assumption.
apply col_permutation_4.
assumption.
assumption.
assumption.
Qed.
Lemma midpoint_diff : forall A M B, A <> B -> is_midpoint M A B -> A <> M /\ B <> M.
intros.
split; intro;subst M.
apply is_midpoint_id in H0.
contradiction.
apply l7_2 in H0.
apply is_midpoint_id in H0.
apply sym_equal in H0.
contradiction.
Qed.
Lemma midpoint_col : forall A M B, is_midpoint M A B -> Col M A B.
intros.
unfold Col.
right;right.
apply mid_bet.
apply l7_2.
assumption.
Qed.
Lemma image_col : forall A B X, Col A B X -> is_image X X A B.
intros.
unfold is_image.
split.
exists X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
Qed.
Lemma l10_12 : forall A B C A' B' C',
Per A B C -> Per A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
intros.
induction (eq_dec_points B C).
subst B.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst B'.
assumption.
induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst B'.
assumption.
assert (exists X, is_midpoint X B B').
apply midpoint_existence.
ex_and H5 X.
double A' X A1.
double C' X C1.
assert(Cong_3 A' B' C' A1 B C1).
repeat split.
eapply l7_13.
apply l7_2.
apply H5.
assumption.
eapply l7_13.
apply l7_2.
apply H5.
apply l7_2.
assumption.
eapply l7_13.
apply H6.
apply l7_2.
assumption.
assert (Per A1 B C1).
eapply l8_10.
apply H0.
apply H8.
unfold Cong_3 in H8.
spliter.
assert(Cong A B A1 B).
eapply cong_transitivity.
apply H1.
assumption.
assert(Cong B C B C1).
eapply cong_transitivity.
apply H2.
assumption.
assert(exists Y, is_midpoint Y C C1).
apply midpoint_existence.
ex_and H14 Y.
apply cong_symmetry.
eapply cong_transitivity.
apply H10.
induction (eq_dec_points B Y).
subst Y.
induction (eq_dec_points A A1).
subst A1.
unfold Per in H9.
ex_and H9 C2.
assert (C=C2).
eapply l7_9.
apply H15.
apply l7_2.
assumption.
subst C2.
assumption.
assert(C1 <> B).
intro.
subst C1.
apply l7_2 in H15.
apply is_midpoint_id in H15.
contradiction.
assert (Per C B A1).
eapply (l8_3 C1 B A1 C).
apply l8_2.
apply H9.
assumption.
apply midpoint_col.
apply l7_2.
assumption.
assert(Col A A1 B).
eapply per_per_col.
apply H.
assumption.
apply l8_2.
assumption.
assert (A= A1 \/ is_midpoint B A A1).
eapply l7_20.
apply col_permutation_5.
assumption.
apply cong_commutativity.
assumption.
induction H19.
contradiction.
eapply l7_13.
apply H19.
assumption.
assert(is_image C1 C B Y).
unfold is_image.
split.
exists Y.
split.
assumption.
apply col_trivial_2.
induction(eq_dec_points C C1).
right.
assumption.
left.
apply perp_sym.
assert(C<>Y /\ C1 <> Y).
eapply midpoint_diff.
assumption.
assumption.
spliter.
eapply per_perp.
assumption.
auto.
assumption.
auto.
apply midpoint_col.
assumption.
unfold Per.
exists C1.
split.
assumption.
assumption.
induction (classic (is_image A A1 B Y)).
eapply l10_10.
2:apply H17.
assumption.
apply l10_4.
assumption.
assert(exists A2, is_image A1 A2 B Y).
apply l10_6_existence.
assumption.
ex_elim H18 A2.
assert (Cong C A2 C1 A1).
eapply l10_10.
2:apply H16.
assumption.
assumption.
assert (Per A2 B C).
eapply (image_preserves_per A1 B C1 A2 B C).
2:apply H19.
assumption.
apply image_col.
apply col_trivial_3.
assumption.
assumption.
assert (Cong A1 B A2 B).
eapply image_col_cong.
apply H19.
apply col_trivial_3.
assert (A = A2 \/ is_midpoint B A A2).
eapply l7_20.
apply col_permutation_1.
eapply per_per_col.
apply H20.
assumption.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply H12.
apply cong_commutativity.
assumption.
induction H22.
subst A2.
apply cong_symmetry.
apply cong_commutativity.
assumption.
assert(Cong A C A2 C).
apply l8_2 in H.
unfold Per in H.
ex_and H A3.
assert(A2=A3).
eapply midpoint_id.
apply H22.
apply H.
subst A3.
apply cong_commutativity.
assumption.
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H18.
apply cong_symmetry.
assumption.
Qed.
Lemma l10_14 : forall P P' A B, P <> P' -> is_image P P' A B -> two_sides A B P P'.
apply osym_two_sides.
Qed.
Lemma l10_15 : forall A B C P, A <> B -> Col A B C -> ~ Col A B P -> exists Q, Perp A B Q C /\ one_side A B P Q.
intros.
assert (exists X , two_sides A B P X).
apply l9_10.
assumption.
intro.
apply H1.
apply col_permutation_1.
assumption.
ex_elim H2 X.
induction (eq_dec_points A C).
subst C.
assert (exists Q, exists T, Perp A B Q A /\ Col A B T /\ Bet X T Q).
apply l8_21.
assumption.
ex_elim H2 Q.
ex_and H4 T.
exists Q.
split.
assumption.
eapply l9_8_1.
apply H3.
unfold two_sides.
repeat split.
assumption.
apply perp_not_col in H2.
intro.
apply H2.
apply col_permutation_1.
assumption.
unfold two_sides in H3.
spliter.
assumption.
exists T.
split.
apply col_permutation_2.
assumption.
apply between_symmetry.
assumption.
assert (exists Q, exists T, Perp C A Q C /\ Col C A T /\ Bet X T Q).
apply l8_21.
auto.
ex_elim H4 Q.
ex_and H5 T.
exists Q.
split.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_5.
assumption.
eapply l9_8_1.
apply H3.
unfold two_sides.
repeat split.
assumption.
eapply perp_not_col in H4.
intro.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
assumption.
unfold two_sides in H3.
spliter.
assumption.
exists T.
split.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
apply col_permutation_5.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
Qed.
Lemma l9_17 : forall A B C P Q, one_side P Q A C -> Bet A B C -> one_side P Q A B.
intros.
induction (eq_dec_points A C).
subst C.
apply between_identity in H0.
subst B.
assumption.
assert( HH:= H).
unfold one_side in H.
ex_and H D.
assert(HH1:=H).
unfold two_sides in H.
unfold two_sides in H2.
spliter.
ex_and H8 X.
ex_and H5 Y.
assert (exists T, Bet B T D /\ Bet X T Y).
eapply l3_17.
apply H9.
apply H10.
assumption.
ex_and H11 T.
unfold one_side.
exists D.
split.
assumption.
unfold two_sides.
repeat split.
assumption.
apply l9_9_bis in HH.
intro.
apply HH.
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists B.
split.
assumption.
assumption.
unfold two_sides in HH1.
spliter.
assumption.
exists T.
induction (classic(Col A C D)).
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H8.
unfold Col.
right; left.
apply H9.
apply col_permutation_1.
assumption.
eapply (col_transitivity_1 _ C).
intro.
subst D.
apply between_identity in H10.
subst Y.
apply H3.
assumption.
apply col_permutation_3.
assumption.
unfold Col.
right; left.
assumption.
intro.
apply H7.
apply col_permutation_4.
assumption.
intro.
subst D.
assert (one_side P Q A A).
apply one_side_reflexivity.
assumption.
apply l9_9_bis in H14.
contradiction.
subst Y.
apply between_identity in H12.
subst X.
split.
assumption.
assumption.
split.
assert (X <> Y).
intro.
subst Y.
apply between_identity in H12.
subst X.
apply H13.
apply col_permutation_1.
eapply (col_transitivity_1 _ T).
intro.
subst D.
contradiction.
unfold Col.
left.
apply between_symmetry.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
eapply col_col.
apply H14.
unfold Col.
right; left.
apply between_symmetry.
assumption.
eapply col_col.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_trivial_3.
eapply col_col.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_trivial_2.
assumption.
Qed.
Lemma l9_18 : forall X Y A B P,X <> Y -> Col X Y P -> Col A B P -> (two_sides X Y A B <-> (Bet A P B /\ ~Col X Y A /\ ~Col X Y B)).
intros.
split.
intros.
unfold two_sides in H2.
spliter.
ex_and H5 T.
assert (P=T).
eapply inter_unicity.
apply H0.
apply H1.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H3.
apply col_permutation_4.
assumption.
intro.
subst B.
apply between_identity in H6.
subst A.
contradiction.
subst T.
repeat split.
assumption.
intro.
apply H3.
apply col_permutation_2.
assumption.
intro.
apply H4.
apply col_permutation_2.
assumption.
intro.
unfold two_sides.
spliter.
repeat split.
assumption.
intro.
apply H3.
apply col_permutation_1.
assumption.
intro.
apply H4.
apply col_permutation_1.
assumption.
exists P.
split.
apply col_permutation_2.
assumption.
assumption.
Qed.
Lemma l9_19 : forall X Y A B P , X <> Y -> Col X Y P -> Col A B P -> (one_side X Y A B <-> (out P A B /\ ~Col X Y A)).
intros.
split.
intro.
assert (HH2:=H2).
unfold one_side in H2.
ex_and H2 D.
unfold two_sides in *.
spliter.
ex_and H6 M.
ex_and H9 N.
split.
unfold out.
repeat split.
intro.
subst P.
apply H7.
apply col_permutation_2.
assumption.
intro.
subst P.
apply H4.
apply col_permutation_2.
assumption.
unfold Col in H1.
induction H1.
right.
apply between_symmetry.
assumption.
induction H1.
apply False_ind.
assert (two_sides X Y A B).
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists P.
split.
apply col_permutation_2.
assumption.
apply between_symmetry.
assumption.
apply l9_9_bis in HH2.
contradiction.
left.
assumption.
intro.
apply H7.
apply col_permutation_2.
assumption.
intros.
spliter.
assert (exists D, two_sides X Y A D).
apply l9_10.
assumption.
intro.
apply H3.
apply col_permutation_1.
assumption.
ex_elim H4 D.
unfold one_side.
exists D.
split.
assumption.
eapply l9_5.
apply H5.
apply col_permutation_2.
apply H0.
assumption.
Qed.
Lemma l10_16 : forall A B C A' B' P, ~Col A B C -> ~ Col A' B' P -> Cong A B A' B' ->
exists C', Cong_3 A B C A' B' C' /\ one_side A' B' P C' .
intros.
induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply False_ind.
apply H.
apply col_trivial_1.
assert(exists X, Col A B X /\ Perp A B C X).
apply l8_18_existence.
assumption.
ex_and H3 X.
assert (exists X', Cong_3 A B X A' B' X').
eapply l4_14.
assumption.
assumption.
ex_elim H5 X'.
assert (exists Q, Perp A' B' Q X' /\ one_side A' B' P Q).
apply l10_15.
intro.
subst B'.
apply H0.
apply col_trivial_1.
eapply l4_13.
apply H3.
assumption.
assumption.
ex_and H5 Q.
assert (exists C', out X' C' Q /\ Cong X' C' X C).
eapply l6_11_existence.
apply perp_distinct in H5.
spliter.
assumption.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
ex_and H8 C'.
exists C'.
unfold Cong_3 in *.
spliter.
assert (Cong A C A' C').
induction(eq_dec_points A X).
subst X.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst X'.
apply cong_symmetry.
assumption.
eapply l10_12.
3: apply H10.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H10.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;assumption.
apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.
assert (Cong B C B' C').
induction(eq_dec_points B X).
subst X.
apply cong_symmetry in H11.
apply cong_identity in H11.
subst X'.
apply cong_symmetry.
assumption.
eapply l10_12.
3: apply H11.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_comm.
apply H4.
apply col_permutation_4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H11.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
apply col_permutation_4.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.
repeat split.
assumption.
assumption.
assumption.
assert (T19 := (l9_19 A' B' C' Q X')).
assert (one_side A' B' C' Q <-> out X' C' Q /\ ~ Col A' B' C').
apply T19.
intro.
subst B'.
apply cong_identity in H1.
contradiction.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.
apply col_permutation_1.
apply out_col.
assumption.
apply cong_symmetry in H1.
destruct H14.
spliter.
assert (one_side A' B' C' Q).
apply H15.
split.
assumption.
intro.
apply H.
eapply l4_13.
apply H16.
unfold Cong_3.
repeat split.
assumption.
apply cong_symmetry.
assumption.
apply cong_symmetry.
assumption.
eapply one_side_transitivity.
apply H7.
apply one_side_symmetry.
assumption.
Qed.
End T10.
Section T10.
Context `{MT:Tarski}.
Ltac assert_cols :=
repeat
match goal with
| H:Bet ?X1 ?X2 ?X3 |- _ =>
not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
end.
Ltac clean_trivial_hyps :=
repeat
match goal with
| H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
| H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
| H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
| H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
| H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
| H:(Col ?X1 ?X1 ?X2) |- _ => clear H
| H:(Col ?X2 ?X1 ?X1) |- _ => clear H
| H:(Col ?X1 ?X2 ?X1) |- _ => clear H
end.
Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
match goal with
| H:(?X1 = ?X2) |- _ => smart_subst X2
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.
Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].
Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.
Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Ltac double A B A' :=
assert (mp:= mdp A B);
elim mp; intros A' ; intro; clear mp.
Definition is_image := fun P' P A B =>
(exists X, is_midpoint X P P' /\ Col A B X) /\ (Perp A B P P' \/ P=P').
Lemma ex_sym : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\ (exists M, Col A B M /\ is_midpoint M X Y).
intros.
induction (classic (Col A B X)).
exists X.
split.
right.
reflexivity.
exists X.
split.
assumption.
apply l7_3_2.
assert (exists M, Col A B M /\ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H0 M.
double X M Z.
exists Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
exists M.
split.
assumption.
assumption.
Qed.
Lemma ex_sym1 : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\ (exists M, Col A B M /\ is_midpoint M X Y /\ is_image X Y A B).
intros.
induction (classic (Col A B X)).
exists X.
split.
right.
reflexivity.
exists X.
split.
assumption.
split.
apply l7_3_2.
unfold is_image.
split.
exists X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
assert (exists M, Col A B M /\ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H0 M.
double X M Z.
exists Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
exists M.
split.
assumption.
split.
assumption.
unfold is_image.
split.
exists M.
split.
apply l7_2.
assumption.
assumption.
left.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst X.
apply l7_3 in H2.
subst Z.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply mid_bet.
assumption.
Qed.
Ltac ex_elim' H x := elim H; intros x ; clear H; intro H.
Ltac spliter1 :=
match goal with
| H:(?X1 /\ ?X2) |- _ => induction H
end.
Ltac ex_and' H x y := ex_elim H x y ; elim y.
Ltac symmetric X A B Y M :=
assert(Hsym := ex_sym1 A B X);
elim Hsym;
intro Y;
clear Hsym;
intro Hsym;
elim Hsym;
intro Hsym1;
intro Hsym2;
elim Hsym2;
intro M;
clear Hsym2;
intro Hsym2;
elim Hsym2;
clear Hsym2;
intro Hsym2;
intro Hsym3;
elim Hsym3;
clear Hsym3;
intro Hsym3;
intro Hsym4;
clear Hsym.
Lemma test : forall A B, (exists X, Col A B X) -> Col A A A.
intros.
ex_elim' H X.
apply col_trivial_1.
Qed.
Lemma l10_2_unicity : forall A B P P1 P2,
A<>B -> is_image P1 P A B -> is_image P2 P A B -> P1=P2.
intros.
unfold is_image in *.
spliter.
ex_and H0 X.
ex_and H1 Y.
induction H2; induction H3.
assert (P <> X).
intro.
subst X.
apply is_midpoint_id in H0.
subst P1.
apply perp_distinct in H3.
spliter.
absurde.
assert (P <> Y).
intro.
subst Y.
apply is_midpoint_id in H1.
subst P2.
apply perp_distinct in H2.
spliter.
absurde.
assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
induction (eq_dec_points X A).
subst X.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.
assert (Y = A).
eapply l8_18_unicity.
apply H10.
assumption.
apply perp_sym.
assumption.
apply col_trivial_3.
apply perp_sym.
assumption.
subst Y.
eapply symmetric_point_unicity.
apply H0.
apply H1.
assert (~ Col A B P /\ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
assert (Y = X).
eapply l8_18_unicity.
apply H11.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Y.
eapply symmetric_point_unicity.
apply H0.
apply H1.
subst P1.
assert (P <> Y).
intro.
subst Y.
apply l7_3 in H0.
subst X.
apply is_midpoint_id in H1.
subst P2.
eapply perp_distinct in H2.
spliter.
absurde.
assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l7_3 in H0.
subst X.
induction (eq_dec_points Y A).
subst Y.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto;
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
assert (~ Col A B P /\ Per P Y A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
subst P2.
assert (P <> X).
intro.
subst X.
apply l7_3 in H1.
subst Y.
apply is_midpoint_id in H0.
subst P1.
eapply perp_distinct in H3.
spliter.
absurde.
assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l7_3 in H1.
subst Y.
induction (eq_dec_points X A).
subst X.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
assert (~ Col A B P /\ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.
subst P1.
subst P2.
reflexivity.
Qed.
Lemma l10_2_existence : forall A B P, exists P', is_image P' P A B.
intros.
induction (eq_dec_points A B).
subst B.
unfold is_image.
exists P.
split.
exists P.
split.
eapply l7_3_2.
apply col_trivial_1.
right.
reflexivity.
induction (classic (Col A B P)).
unfold is_image.
exists P.
split.
exists P.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
assert (exists X, Col A B X /\ Perp A B P X).
eapply l8_18_existence.
assumption.
ex_and H1 X.
double P X P'.
exists P'.
unfold is_image.
split.
exists X.
split; assumption.
left.
apply perp_sym.
eapply perp_col.
intro.
subst P'.
apply l7_3 in H3.
subst X.
apply perp_distinct in H2.
spliter.
absurde.
apply perp_sym.
apply H2.
unfold Col.
left.
apply mid_bet.
assumption.
Qed.
Lemma l10_4 : forall A B P P', is_image P P' A B -> is_image P' P A B.
intros.
unfold is_image in *.
spliter.
ex_and H X.
split.
exists X.
split.
apply l7_2.
assumption.
assumption.
induction H0.
left.
apply perp_right_comm.
assumption.
right.
subst P'.
reflexivity.
Qed.
Lemma l10_5 : forall A B P P' P'', A<>B -> is_image P' P A B -> is_image P'' P' A B -> P=P''.
Proof.
intros.
eapply l10_2_unicity.
apply H.
eapply l10_4.
apply H0.
assumption.
Qed.
Lemma l10_6_unicity : forall A B P P1 P2, A<>B -> is_image P P1 A B -> is_image P P2 A B -> P1 = P2.
intros.
eapply l10_2_unicity.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H1.
Qed.
Lemma l10_6_existence : forall A B P', A<>B -> exists P, is_image P' P A B.
intros.
assert (exists P, is_image P P' A B).
eapply l10_2_existence.
ex_and H0 P.
exists P.
apply l10_4.
assumption.
Qed.
Lemma l10_7 : forall A B P P' Q Q', A<>B -> is_image P' P A B -> is_image Q' Q A B -> P'=Q' -> P = Q.
intros.
subst Q'.
eapply l10_2_unicity.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H1.
Qed.
Lemma l10_8 : forall A B P, A<>B -> is_image P P A B -> Col P A B.
intros.
unfold is_image in H0.
spliter.
ex_and H0 X.
apply l7_3 in H0.
subst X.
apply col_permutation_2.
assumption.
Qed.
Lemma perp_col2 : forall A B C D X Y, Perp A B X Y -> C <> D -> Col A B C -> Col A B D -> Perp C D X Y.
intros.
assert(HH:=H).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points A C).
subst A.
eapply perp_col.
assumption.
apply H.
assumption.
assert(Perp A C X Y).
eapply perp_col.
assumption.
apply H.
assumption.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H6.
apply col_permutation_2;
eapply col2.
apply H3.
assumption.
assumption.
Qed.
Lemma image_col_cong : forall A B P P' X, is_image P P' A B -> Col A B X -> Cong P X P' X.
intros.
unfold is_image in H.
spliter.
ex_and H M.
induction H1.
assert (HH:= H1).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points M X).
subst X.
unfold is_midpoint in H.
spliter.
apply cong_symmetry.
apply cong_right_commutativity.
assumption.
assert (Perp M X P' P).
eapply perp_col2.
apply H1.
apply H5.
assumption.
assumption.
assert(~ Col A B P /\ Per P M X).
eapply l8_16_1.
assumption.
assumption.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
subst P.
apply l7_2 in H.
apply is_midpoint_id in H.
subst P'.
absurde.
apply perp_left_comm.
apply perp_sym.
apply H1;
eapply perp_left_comm.
unfold Col.
right; left.
apply mid_bet.
assumption.
spliter.
eapply l8_2 in H8.
unfold Per in H8.
ex_and H8 P0.
assert (P0 = P').
eapply symmetric_point_unicity.
apply H8.
apply l7_2.
assumption.
subst P0.
apply cong_commutativity.
assumption.
subst P'.
apply cong_reflexivity.
Qed.
Lemma perp_not_col : forall A B P, Perp A B P A -> ~ Col A B P.
intros.
assert (Perp_in A A B P A).
apply perp_perp_in.
assumption.
assert (Per P A B).
apply perp_in_per.
apply perp_in_sym.
assumption.
apply perp_in_left_comm in H0.
assert (~ Col B A P -> ~ Col A B P).
intro.
intro.
apply H2.
apply col_permutation_4.
assumption.
apply H2.
apply perp_distinct in H.
spliter.
apply per_not_col.
auto.
auto.
apply perp_in_per.
apply perp_in_right_comm.
assumption.
Qed.
Lemma osym_two_sides : forall P P' A B, P <> P' -> is_image P P' A B -> two_sides A B P P'.
intros.
unfold is_image in H0.
spliter.
ex_and H0 M.
induction H1.
Focus 2.
subst P'.
absurde.
assert (P <> M).
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
induction (eq_dec_points A M).
subst A.
assert (Perp M B P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.
apply perp_sym.
apply perp_right_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (Perp_in M M B P M).
eapply perp_perp_in.
assumption.
assert(Per B M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.
assert (B <> M).
intro.
repeat split.
subst B.
apply perp_distinct in H1.
spliter.
absurde.
assert (~Col B M P).
eapply per_not_col.
assumption.
auto.
assumption.
repeat split.
auto.
intro.
apply H8.
apply col_permutation_3.
assumption.
intro.
apply H8.
apply col_permutation_2.
eapply (col2 _ P').
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_4.
assumption.
exists M.
split.
apply col_trivial_1.
apply mid_bet.
apply l7_2.
assumption.
induction (eq_dec_points B M).
subst B.
assert (Perp M A P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.
apply perp_sym.
apply perp_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (Perp_in M M A P M).
eapply perp_perp_in.
assumption.
assert(Per A M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.
repeat split.
assumption.
assert (~Col A M P).
eapply per_not_col.
assumption.
auto.
assumption.
intro.
apply H8.
apply col_permutation_1.
assumption.
intro.
assert (Col M A P).
eapply (col_transitivity_1 _ P').
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
apply col_permutation_2.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
eapply (per_not_col ).
3: apply H7.
assumption.
auto.
apply col_permutation_4.
assumption.
exists M.
split.
apply col_trivial_3.
apply mid_bet.
apply l7_2.
assumption.
repeat split.
apply perp_distinct in H1.
spliter.
assumption.
assert(Perp P M A B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_right_comm.
apply H1.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (~ Col M P A).
apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H6.
assumption.
intro.
apply H7.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H1.
spliter.
apply H1.
assumption.
apply col_permutation_1.
assumption.
assert(Perp P' M A B).
eapply perp_col.
intro.
subst P'.
apply is_midpoint_id in H0.
subst P.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col M P' A).
apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H6.
assumption.
intro.
apply H7.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H1.
spliter.
apply H1.
assumption.
apply col_permutation_1.
assumption.
exists M.
split.
apply col_permutation_2.
assumption.
apply mid_bet.
apply l7_2.
assumption.
Qed.
Lemma image_id : forall A B T T', Col A B T -> is_image T T' A B -> T = T'.
intros.
unfold is_image in H0.
spliter.
ex_and H0 X.
induction H1.
assert (A <> B /\ T' <> T).
apply perp_distinct in H1.
spliter.
split;
assumption.
spliter.
Focus 2.
subst T'.
reflexivity.
induction (eq_dec_points A X).
subst X.
assert (Perp A B T' A).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst A.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col A T' B).
apply perp_not_col.
apply perp_comm.
apply perp_sym.
assumption.
assert (A = T).
eapply inter_unicity.
5: apply H6.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
assumption.
apply col_trivial_2.
assumption.
subst A.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
induction (eq_dec_points B X).
subst X.
assert (Perp A B T' B).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst B.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col B T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
assumption.
assert (B = T).
eapply inter_unicity.
5: apply H7.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst B.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
assert (Col A X T).
eapply col_transitivity_1.
apply H3.
assumption.
assumption.
assert (Perp A B T' X).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H0.
subst X.
absurde.
apply perp_sym.
apply H1.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
assert (~ Col X T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
eapply perp_col.
assumption.
apply H8.
assumption.
assert (X = T).
eapply inter_unicity.
5: apply H9.
apply col_trivial_3.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
apply H0.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst X.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst T'.
absurde.
Qed.
Lemma osym_not_col : forall A B P P', is_image P P' A B -> ~ Col A B P -> ~ Col A B P'.
intros.
assert ( HH:= H).
unfold is_image in HH.
spliter.
ex_and H1 T.
intro.
induction H2.
assert (P'=P).
eapply image_id.
apply H4.
apply l10_4.
assumption.
subst P'.
apply perp_distinct in H2.
spliter.
absurde.
apply H0.
subst P'.
assumption.
Qed.
Lemma cong_cong_half : forall A M B A' M' B', is_midpoint M A B -> is_midpoint M' A' B' -> Cong A B A' B' -> Cong A M A' M'.
intros.
unfold is_midpoint in *.
spliter.
assert(exists M'', Bet A' M'' B' /\ Cong_3 A M B A' M'' B').
eapply l4_5.
assumption.
assumption.
ex_and H4 M''.
assert (is_midpoint M'' A' B').
unfold is_midpoint.
split.
assumption.
unfold Cong_3 in H5.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
eapply cong_transitivity.
apply H3.
assumption.
assert(M'=M'').
eapply l7_17;
unfold is_midpoint;
split.
apply H0.
apply H2.
apply H4.
unfold is_midpoint in H6.
spliter.
assumption.
subst M''.
unfold Cong_3 in H5.
spliter.
assumption.
Qed.
Lemma image_cong_col : forall A B P P' X, P <> P' -> is_image P P' A B -> Cong P X P' X -> Col A B X.
intros.
unfold is_image in H0.
spliter.
ex_and H0 M.
induction H2.
Focus 2.
subst P'.
absurde.
induction(eq_dec_points A M).
subst M.
assert (Perp P A A B).
eapply perp_col.
apply perp_distinct in H2.
spliter.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H2.
unfold Col.
right; left.
apply mid_bet.
assumption.
apply perp_comm in H4.
apply perp_perp_in in H4.
apply perp_in_comm in H4.
apply perp_in_per in H4.
assert (Per X A P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply l8_2 in H4.
apply col_permutation_2.
eapply per_per_col.
apply H4.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
assumption.
assert (Perp P M M A).
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
apply perp_sym.
apply perp_comm.
eapply perp_col.
assumption.
apply H2.
assumption.
unfold Col.
right; left.
apply mid_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 M P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply l8_2 in H5.
assert (Col A X M).
eapply per_per_col.
apply H5.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
assumption.
eapply col_transitivity_1.
apply H4.
apply col_permutation_5.
assumption.
apply col_permutation_5.
assumption.
Qed.
Lemma midpoint_preserves_image : forall A B P P' Q Q' M, A <> B -> Col A B M ->is_image P P' A B
-> is_midpoint M P Q -> is_midpoint M P' Q' -> is_image Q Q' A B.
intros.
assert (HH1:=H1).
unfold is_image in H1.
spliter.
ex_and H1 X.
induction H4.
double X M Y.
assert (is_midpoint Y Q Q').
eapply symmetry_preserves_midpoint.
apply H2.
apply H6.
apply H3.
apply l7_2.
apply H1.
assert (P <> P').
intro.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.
assert (Q <> Q').
intro.
subst Q'.
apply l7_3 in H7.
subst Q.
assert (P=P').
eapply l7_9.
apply H2.
apply H3.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.
split.
exists Y.
split.
apply l7_2.
apply H7.
induction (eq_dec_points X Y).
subst Y.
assumption.
eapply (colx _ _ M X).
assumption.
intro.
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
assumption.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
left.
assert(Per M Y Q).
unfold Per.
exists Q'.
split.
assumption.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H14.
apply cong_symmetry.
eapply cong_transitivity.
apply cong_symmetry.
apply H13.
eapply image_col_cong.
apply l10_4.
apply HH1.
assumption.
induction (eq_dec_points X Y).
subst Y.
apply l7_3 in H6.
subst X.
apply perp_sym.
eapply perp_col.
auto.
apply perp_left_comm.
eapply perp_col.
2:apply perp_sym.
2:apply H4.
intro.
subst Q'.
apply l7_3 in H3.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
eapply (col_transitivity_2 M).
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
eapply (col_transitivity_2 M).
intro.
subst Q'.
apply l7_2 in H7.
apply is_midpoint_id in H7.
subst Q.
absurde.
unfold Col.
right; right.
apply mid_bet.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
apply per_perp_in in H10.
apply perp_in_perp in H10.
induction H10.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_comm.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_comm.
eapply (perp_col Y Q).
intro.
subst Q.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_sym.
induction (eq_dec_points A M).
subst A.
apply perp_left_comm.
eapply (perp_col _ M).
auto.
apply perp_left_comm.
eapply (perp_col _ Y).
assumption.
assumption.
induction (eq_dec_points M X).
subst X.
apply is_midpoint_id in H6.
subst M.
apply col_trivial_1.
eapply (col2 _ X).
assumption.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_5.
assumption.
apply col_trivial_2.
induction (eq_dec_points B M).
subst M.
apply perp_left_comm.
apply (perp_col _ Y).
auto.
assumption.
induction (eq_dec_points B X).
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
eapply col_transitivity_1.
apply H13.
unfold Col.
right; right.
apply mid_bet.
apply l7_2.
assumption.
apply col_permutation_1.
assumption.
eapply perp_col.
assumption.
apply perp_left_comm.
eapply (perp_col M Y).
auto.
assumption.
assert(Col B X M).
eapply col_transitivity_2.
apply H.
assumption.
assumption.
induction (eq_dec_points M X).
subst X.
apply is_midpoint_id in H6.
contradiction.
assert(Col B Y M).
apply col_permutation_1.
eapply (col_transitivity_2 X).
auto.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (col_transitivity_1 _ B).
auto.
apply col_permutation_2.
assumption.
apply col_permutation_3.
apply H0.
apply col_permutation_5.
apply H0.
apply col_trivial_2.
unfold Col.
left.
apply mid_bet.
apply H7.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
intro.
subst Q.
apply is_midpoint_id in H7.
subst Q'.
absurde.
subst P'.
apply l7_3 in H1.
subst P.
assert(Q = Q').
eapply l7_9.
apply l7_2.
apply H2.
apply l7_2.
apply H3.
subst Q'.
split.
exists Q.
split.
apply l7_3_2.
induction (eq_dec_points M X).
subst X.
assert(M=Q).
apply is_midpoint_id.
assumption.
subst Q.
assumption.
eapply colx.
assumption.
apply H1.
intro.
subst Q.
apply l7_3 in H2.
contradiction.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
apply H3.
right.
reflexivity.
Qed.
Definition is_image_in := fun M P' P A B =>
(is_midpoint M P P' /\ Col A B M) /\ (Perp A B P P' \/ P=P').
Lemma image_in_is_image : forall M A B P P' , is_image_in M P P' A B -> is_image P P' A B.
intros.
unfold is_image_in in H.
spliter.
unfold is_image.
split.
exists M.
split;
assumption.
assumption.
Qed.
Lemma image_image_in : forall A B P P' M, P <> P'-> is_image P P' A B -> Col A B M -> Col P M P' -> is_image_in M P P' A B.
intros.
unfold is_image_in.
split.
split.
assert(HH:=H0).
unfold is_image in H0.
spliter.
ex_and H0 M'.
induction H3.
assert (Perp P M' A B).
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H3.
unfold Col.
right; left.
apply mid_bet.
assumption.
assert (M'=M).
eapply inter_unicity.
apply H4.
unfold Col.
right; left.
apply mid_bet.
apply H0.
assumption.
apply col_permutation_5.
assumption.
induction (eq_dec_points A M').
subst M'.
assert (~ Col A B P /\ Per P A B).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
apply col_trivial_3.
apply col_trivial_2.
apply perp_distinct in H3.
spliter.
auto.
apply perp_sym.
assumption.
spliter.
intro.
apply H6.
apply col_permutation_5.
assumption.
assert (~ Col A B P /\ Per P M' A).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
assumption.
apply col_trivial_3.
assumption.
apply perp_sym.
assumption.
spliter.
intro.
apply H7.
apply col_permutation_5.
assumption.
apply perp_distinct in H3.
spliter.
auto.
subst M'.
assumption.
subst P'.
absurde.
assumption.
assert (HH:=H0).
unfold is_image in H0.
spliter.
induction H3.
left.
assumption.
right.
assumption.
Qed.
Lemma image_in_col : forall A B P P' Q Q' M, is_image_in M P P' A B -> is_image_in M Q Q' A B -> Col M P Q.
intros.
assert(is_image P P' A B).
eapply (image_in_is_image M).
assumption.
assert(is_image Q Q' A B).
eapply (image_in_is_image M).
assumption.
unfold is_image_in in *.
spliter.
induction H3.
induction H5.
induction (eq_dec_points A M).
subst M.
assert (Per B A P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H1.
apply col_trivial_2.
assert (Per B A Q).
unfold Per.
exists Q'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H2.
apply col_trivial_2.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H7.
apply perp_distinct in H3.
spliter.
assumption.
apply l8_2.
assumption.
assert (Per A M P).
unfold Per.
exists P'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H1.
apply col_trivial_3.
assert (Per A M Q).
unfold Per.
exists Q'.
split.
apply l7_2.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H2.
apply col_trivial_3.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H8.
auto.
apply l8_2.
assumption.
subst P'.
apply l7_3 in H.
subst P.
apply col_trivial_1.
subst Q'.
apply l7_3 in H0.
subst Q.
apply col_trivial_3.
Qed.
Lemma image_in_col0 : forall A B P P' Y : Tpoint, is_image_in Y P P' A B -> Col P P' Y.
intros.
apply col_permutation_1.
eapply (image_in_col A B P P').
assumption.
assert (HH:=H).
apply image_in_is_image in H.
unfold is_image_in in HH.
spliter.
induction H1.
apply l10_4 in H.
eapply (image_image_in _ _ _ P ).
apply perp_distinct in H1.
spliter.
assumption.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
subst P'.
apply l7_3 in H0.
subst P.
unfold is_image_in.
repeat split.
apply between_trivial2.
apply cong_trivial_identity.
assumption.
right.
reflexivity.
Qed.
Lemma l10_10 : forall A B P Q P' Q', A<>B -> is_image P' P A B -> is_image Q' Q A B -> Cong P Q P' Q'.
intros.
intros.
assert(HH0 := H0).
assert(HH1 := H1 ).
unfold is_image in H0.
unfold is_image in H1.
spliter.
ex_and H0 X.
ex_and H1 Y.
assert (exists M, is_midpoint M X Y).
apply midpoint_existence.
ex_elim H6 M.
double P M P''.
double Q M Q''.
double P' M P'''.
apply cong_commutativity.
induction H3.
Focus 2.
subst P'.
apply l7_3 in H0.
subst P.
eapply image_col_cong.
apply l10_4.
apply HH1.
assumption.
induction H2.
Focus 2.
subst Q'.
apply l7_3 in H1.
subst Q.
apply cong_commutativity.
eapply image_col_cong.
apply l10_4.
apply HH0.
assumption.
assert (is_image P'' P''' A B).
eapply (midpoint_preserves_image _ _ _ _ _ _ M).
assumption.
induction (eq_dec_points X Y).
subst Y.
apply l7_3 in H7.
subst X.
assumption.
assert(Col A X Y).
eapply col_transitivity_1.
apply H.
assumption.
assumption.
assert(Col B X Y).
eapply (col_transitivity_1 _ A).
auto.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
eapply col_col.
apply H10.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply l10_4.
apply HH0.
assumption.
assumption.
assert(P'' <> P''').
intro.
subst P'''.
assert( P' = P).
eapply l7_9.
apply H9.
assumption.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
assert (is_midpoint Y P'' P''').
eapply symmetry_preserves_midpoint.
apply H6.
apply H7.
apply H9.
assumption.
assert (Cong P'' Y P''' Y).
unfold is_midpoint in H12.
spliter.
apply cong_right_commutativity.
assumption.
assert (Cong Q Y Q' Y).
unfold is_midpoint in H1.
spliter.
apply cong_right_commutativity.
assumption.
assert (Col P'' Y Q).
apply col_permutation_2.
eapply image_in_col.
eapply image_image_in.
apply perp_distinct in H2.
spliter.
apply H15.
apply l10_4.
apply HH1.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (image_image_in _ _ _ P''').
assumption.
assumption.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.
eapply (l4_16 P'' Y Q P P''' Y Q' P').
repeat split.
assumption.
assumption.
unfold Col in H15.
induction H15.
assert(Bet P''' Y Q').
eapply (l7_15).
apply H12.
apply l7_3_2.
apply H1.
assumption.
eapply l2_l1.
apply H15.
apply H16.
assumption.
apply cong_commutativity.
assumption.
induction H15.
assert (Bet Y Q' P''').
eapply (l7_15).
apply l7_3_2.
apply H1.
apply H12.
assumption.
eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.
apply between_symmetry in H15.
assert (Bet Y P''' Q').
eapply (l7_15).
apply l7_3_2.
apply H12.
apply H1.
assumption.
apply cong_commutativity.
eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.
apply cong_commutativity.
assumption.
assert (Cong P Y P' Y).
eapply image_col_cong.
eapply l10_4.
apply HH0.
assumption.
assert (Cong P P'' P' P''').
induction(eq_dec_points X Y).
subst Y.
eapply l2_l1.
apply mid_bet.
apply H6.
apply H9.
apply l7_3 in H7.
subst X.
assumption.
apply l7_3 in H7.
subst X.
eapply cong_transitivity.
unfold is_midpoint in H6.
spliter.
apply cong_symmetry.
apply H7.
eapply cong_transitivity.
apply H16.
unfold is_midpoint in H9.
spliter.
assumption.
eapply l2_l1.
apply H6.
apply H9.
eapply image_col_cong.
apply l10_4.
apply HH0.
unfold is_midpoint in H7.
spliter.
eapply colx.
assumption.
3:apply H4.
3:apply H5.
auto.
intro.
subst X.
apply cong_symmetry in H18.
apply cong_identity in H18.
subst Y.
absurde.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply H10.
eapply colx.
4:apply H4.
4:apply H5.
assumption.
auto.
intro.
subst X.
apply is_midpoint_id in H7.
contradiction.
unfold Col.
right; left.
apply mid_bet.
apply l7_2.
assumption.
apply cong_commutativity.
assumption.
apply cong_commutativity.
eapply image_col_cong.
apply l10_4.
apply HH0.
assumption.
intro.
subst P''.
apply cong_symmetry in H13.
apply cong_identity in H13.
subst P'''.
absurde.
Qed.
Lemma per_per_cong' : forall 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.
intros.
eapply l7_20.
apply col_permutation_5.
eapply per_per_col.
apply l8_2.
apply H0.
auto.
apply l8_2.
assumption.
assumption.
Qed.
Lemma per_per_cong : forall 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.
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.
split.
exists 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 is_image_rev : forall P P' A B, is_image P P' A B -> is_image P P' B A.
unfold is_image.
intros.
spliter.
split.
ex_and H M.
exists M.
split.
assumption.
apply col_permutation_4.
assumption.
induction H0.
left.
apply perp_left_comm.
assumption.
right.
assumption.
Qed.
Lemma per_double_cong : forall A B C C', Per A B C -> is_midpoint B C C' -> Cong A C A C'.
intros.
unfold Per in H.
ex_and H C''.
assert (C' = C'').
eapply l7_9.
apply l7_2.
apply H0.
apply l7_2.
assumption.
subst C''.
assumption.
Qed.
Lemma midpoint_preserves_per : forall A B C A1 B1 C1 M, Per A B C ->
is_midpoint M A A1 -> is_midpoint M B B1 -> is_midpoint M C C1
-> Per A1 B1 C1.
intros.
unfold Per in *.
ex_and H C'.
double C' M C1'.
exists C1'.
split.
eapply symmetry_preserves_midpoint.
apply H2.
apply H1.
apply H4.
assumption.
eapply l7_16.
apply H0.
apply H2.
apply H0.
apply H4.
assumption.
Qed.
Lemma image_preserves_bet : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> Bet A B C -> Bet A' B' C'.
intros.
eapply l4_6.
apply H3.
unfold Cong_3.
repeat split;
eapply l10_10.
apply H.
apply l10_4;
assumption.
apply l10_4;
assumption.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
Qed.
Lemma image_preserves_midpoint : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> is_midpoint A B C -> is_midpoint A' B' C'.
intros.
unfold is_midpoint in *.
spliter.
repeat split.
eapply image_preserves_bet.
apply H.
apply H1.
apply H0.
apply H2.
assumption.
eapply cong_transitivity.
eapply l10_10.
apply H.
apply H1.
apply H0.
eapply cong_transitivity.
apply H4.
eapply l10_10.
apply H.
apply l10_4.
apply H0.
apply l10_4.
apply H2.
Qed.
Lemma image_preserves_per : forall A B C A' B' C' X Y, X <> Y -> is_image A A' X Y -> is_image B B' X Y -> is_image C C' X Y
-> Per A B C -> Per A' B' C'.
intros.
double C B C1.
assert (exists C1', is_image C1 C1' X Y).
apply l10_6_existence.
assumption.
ex_and H5 C1'.
unfold Per.
exists C1'.
split.
eapply image_preserves_midpoint.
apply H.
apply H1.
apply H2.
apply H6.
assumption.
eapply cong_transitivity.
eapply l10_10.
apply H.
apply H0.
apply H2.
eapply cong_transitivity.
unfold Per in H3.
ex_and H3 C2.
assert (C2=C1).
eapply symmetric_point_unicity.
apply H3.
assumption.
subst C2.
apply H5.
eapply l10_10.
apply H.
apply l10_4.
assumption.
apply l10_4.
assumption.
Qed.
Lemma per_perp : forall A B C D, A <> B -> B <> C -> D <> B -> D <> C -> Col B C D -> Per A B C -> Perp C D A B.
intros.
apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
eapply (perp_col _ B).
auto.
apply perp_sym.
apply perp_right_comm.
assumption.
apply col_permutation_4.
assumption.
assumption.
assumption.
Qed.
Lemma midpoint_diff : forall A M B, A <> B -> is_midpoint M A B -> A <> M /\ B <> M.
intros.
split; intro;subst M.
apply is_midpoint_id in H0.
contradiction.
apply l7_2 in H0.
apply is_midpoint_id in H0.
apply sym_equal in H0.
contradiction.
Qed.
Lemma midpoint_col : forall A M B, is_midpoint M A B -> Col M A B.
intros.
unfold Col.
right;right.
apply mid_bet.
apply l7_2.
assumption.
Qed.
Lemma image_col : forall A B X, Col A B X -> is_image X X A B.
intros.
unfold is_image.
split.
exists X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
Qed.
Lemma l10_12 : forall A B C A' B' C',
Per A B C -> Per A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
intros.
induction (eq_dec_points B C).
subst B.
apply cong_symmetry in H2.
apply cong_identity in H2.
subst B'.
assumption.
induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst B'.
assumption.
assert (exists X, is_midpoint X B B').
apply midpoint_existence.
ex_and H5 X.
double A' X A1.
double C' X C1.
assert(Cong_3 A' B' C' A1 B C1).
repeat split.
eapply l7_13.
apply l7_2.
apply H5.
assumption.
eapply l7_13.
apply l7_2.
apply H5.
apply l7_2.
assumption.
eapply l7_13.
apply H6.
apply l7_2.
assumption.
assert (Per A1 B C1).
eapply l8_10.
apply H0.
apply H8.
unfold Cong_3 in H8.
spliter.
assert(Cong A B A1 B).
eapply cong_transitivity.
apply H1.
assumption.
assert(Cong B C B C1).
eapply cong_transitivity.
apply H2.
assumption.
assert(exists Y, is_midpoint Y C C1).
apply midpoint_existence.
ex_and H14 Y.
apply cong_symmetry.
eapply cong_transitivity.
apply H10.
induction (eq_dec_points B Y).
subst Y.
induction (eq_dec_points A A1).
subst A1.
unfold Per in H9.
ex_and H9 C2.
assert (C=C2).
eapply l7_9.
apply H15.
apply l7_2.
assumption.
subst C2.
assumption.
assert(C1 <> B).
intro.
subst C1.
apply l7_2 in H15.
apply is_midpoint_id in H15.
contradiction.
assert (Per C B A1).
eapply (l8_3 C1 B A1 C).
apply l8_2.
apply H9.
assumption.
apply midpoint_col.
apply l7_2.
assumption.
assert(Col A A1 B).
eapply per_per_col.
apply H.
assumption.
apply l8_2.
assumption.
assert (A= A1 \/ is_midpoint B A A1).
eapply l7_20.
apply col_permutation_5.
assumption.
apply cong_commutativity.
assumption.
induction H19.
contradiction.
eapply l7_13.
apply H19.
assumption.
assert(is_image C1 C B Y).
unfold is_image.
split.
exists Y.
split.
assumption.
apply col_trivial_2.
induction(eq_dec_points C C1).
right.
assumption.
left.
apply perp_sym.
assert(C<>Y /\ C1 <> Y).
eapply midpoint_diff.
assumption.
assumption.
spliter.
eapply per_perp.
assumption.
auto.
assumption.
auto.
apply midpoint_col.
assumption.
unfold Per.
exists C1.
split.
assumption.
assumption.
induction (classic (is_image A A1 B Y)).
eapply l10_10.
2:apply H17.
assumption.
apply l10_4.
assumption.
assert(exists A2, is_image A1 A2 B Y).
apply l10_6_existence.
assumption.
ex_elim H18 A2.
assert (Cong C A2 C1 A1).
eapply l10_10.
2:apply H16.
assumption.
assumption.
assert (Per A2 B C).
eapply (image_preserves_per A1 B C1 A2 B C).
2:apply H19.
assumption.
apply image_col.
apply col_trivial_3.
assumption.
assumption.
assert (Cong A1 B A2 B).
eapply image_col_cong.
apply H19.
apply col_trivial_3.
assert (A = A2 \/ is_midpoint B A A2).
eapply l7_20.
apply col_permutation_1.
eapply per_per_col.
apply H20.
assumption.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply H12.
apply cong_commutativity.
assumption.
induction H22.
subst A2.
apply cong_symmetry.
apply cong_commutativity.
assumption.
assert(Cong A C A2 C).
apply l8_2 in H.
unfold Per in H.
ex_and H A3.
assert(A2=A3).
eapply midpoint_id.
apply H22.
apply H.
subst A3.
apply cong_commutativity.
assumption.
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H18.
apply cong_symmetry.
assumption.
Qed.
Lemma l10_14 : forall P P' A B, P <> P' -> is_image P P' A B -> two_sides A B P P'.
apply osym_two_sides.
Qed.
Lemma l10_15 : forall A B C P, A <> B -> Col A B C -> ~ Col A B P -> exists Q, Perp A B Q C /\ one_side A B P Q.
intros.
assert (exists X , two_sides A B P X).
apply l9_10.
assumption.
intro.
apply H1.
apply col_permutation_1.
assumption.
ex_elim H2 X.
induction (eq_dec_points A C).
subst C.
assert (exists Q, exists T, Perp A B Q A /\ Col A B T /\ Bet X T Q).
apply l8_21.
assumption.
ex_elim H2 Q.
ex_and H4 T.
exists Q.
split.
assumption.
eapply l9_8_1.
apply H3.
unfold two_sides.
repeat split.
assumption.
apply perp_not_col in H2.
intro.
apply H2.
apply col_permutation_1.
assumption.
unfold two_sides in H3.
spliter.
assumption.
exists T.
split.
apply col_permutation_2.
assumption.
apply between_symmetry.
assumption.
assert (exists Q, exists T, Perp C A Q C /\ Col C A T /\ Bet X T Q).
apply l8_21.
auto.
ex_elim H4 Q.
ex_and H5 T.
exists Q.
split.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_5.
assumption.
eapply l9_8_1.
apply H3.
unfold two_sides.
repeat split.
assumption.
eapply perp_not_col in H4.
intro.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
assumption.
unfold two_sides in H3.
spliter.
assumption.
exists T.
split.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
apply col_permutation_5.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
Qed.
Lemma l9_17 : forall A B C P Q, one_side P Q A C -> Bet A B C -> one_side P Q A B.
intros.
induction (eq_dec_points A C).
subst C.
apply between_identity in H0.
subst B.
assumption.
assert( HH:= H).
unfold one_side in H.
ex_and H D.
assert(HH1:=H).
unfold two_sides in H.
unfold two_sides in H2.
spliter.
ex_and H8 X.
ex_and H5 Y.
assert (exists T, Bet B T D /\ Bet X T Y).
eapply l3_17.
apply H9.
apply H10.
assumption.
ex_and H11 T.
unfold one_side.
exists D.
split.
assumption.
unfold two_sides.
repeat split.
assumption.
apply l9_9_bis in HH.
intro.
apply HH.
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists B.
split.
assumption.
assumption.
unfold two_sides in HH1.
spliter.
assumption.
exists T.
induction (classic(Col A C D)).
assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H8.
unfold Col.
right; left.
apply H9.
apply col_permutation_1.
assumption.
eapply (col_transitivity_1 _ C).
intro.
subst D.
apply between_identity in H10.
subst Y.
apply H3.
assumption.
apply col_permutation_3.
assumption.
unfold Col.
right; left.
assumption.
intro.
apply H7.
apply col_permutation_4.
assumption.
intro.
subst D.
assert (one_side P Q A A).
apply one_side_reflexivity.
assumption.
apply l9_9_bis in H14.
contradiction.
subst Y.
apply between_identity in H12.
subst X.
split.
assumption.
assumption.
split.
assert (X <> Y).
intro.
subst Y.
apply between_identity in H12.
subst X.
apply H13.
apply col_permutation_1.
eapply (col_transitivity_1 _ T).
intro.
subst D.
contradiction.
unfold Col.
left.
apply between_symmetry.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
eapply col_col.
apply H14.
unfold Col.
right; left.
apply between_symmetry.
assumption.
eapply col_col.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_trivial_3.
eapply col_col.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_trivial_2.
assumption.
Qed.
Lemma l9_18 : forall X Y A B P,X <> Y -> Col X Y P -> Col A B P -> (two_sides X Y A B <-> (Bet A P B /\ ~Col X Y A /\ ~Col X Y B)).
intros.
split.
intros.
unfold two_sides in H2.
spliter.
ex_and H5 T.
assert (P=T).
eapply inter_unicity.
apply H0.
apply H1.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H3.
apply col_permutation_4.
assumption.
intro.
subst B.
apply between_identity in H6.
subst A.
contradiction.
subst T.
repeat split.
assumption.
intro.
apply H3.
apply col_permutation_2.
assumption.
intro.
apply H4.
apply col_permutation_2.
assumption.
intro.
unfold two_sides.
spliter.
repeat split.
assumption.
intro.
apply H3.
apply col_permutation_1.
assumption.
intro.
apply H4.
apply col_permutation_1.
assumption.
exists P.
split.
apply col_permutation_2.
assumption.
assumption.
Qed.
Lemma l9_19 : forall X Y A B P , X <> Y -> Col X Y P -> Col A B P -> (one_side X Y A B <-> (out P A B /\ ~Col X Y A)).
intros.
split.
intro.
assert (HH2:=H2).
unfold one_side in H2.
ex_and H2 D.
unfold two_sides in *.
spliter.
ex_and H6 M.
ex_and H9 N.
split.
unfold out.
repeat split.
intro.
subst P.
apply H7.
apply col_permutation_2.
assumption.
intro.
subst P.
apply H4.
apply col_permutation_2.
assumption.
unfold Col in H1.
induction H1.
right.
apply between_symmetry.
assumption.
induction H1.
apply False_ind.
assert (two_sides X Y A B).
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists P.
split.
apply col_permutation_2.
assumption.
apply between_symmetry.
assumption.
apply l9_9_bis in HH2.
contradiction.
left.
assumption.
intro.
apply H7.
apply col_permutation_2.
assumption.
intros.
spliter.
assert (exists D, two_sides X Y A D).
apply l9_10.
assumption.
intro.
apply H3.
apply col_permutation_1.
assumption.
ex_elim H4 D.
unfold one_side.
exists D.
split.
assumption.
eapply l9_5.
apply H5.
apply col_permutation_2.
apply H0.
assumption.
Qed.
Lemma l10_16 : forall A B C A' B' P, ~Col A B C -> ~ Col A' B' P -> Cong A B A' B' ->
exists C', Cong_3 A B C A' B' C' /\ one_side A' B' P C' .
intros.
induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply False_ind.
apply H.
apply col_trivial_1.
assert(exists X, Col A B X /\ Perp A B C X).
apply l8_18_existence.
assumption.
ex_and H3 X.
assert (exists X', Cong_3 A B X A' B' X').
eapply l4_14.
assumption.
assumption.
ex_elim H5 X'.
assert (exists Q, Perp A' B' Q X' /\ one_side A' B' P Q).
apply l10_15.
intro.
subst B'.
apply H0.
apply col_trivial_1.
eapply l4_13.
apply H3.
assumption.
assumption.
ex_and H5 Q.
assert (exists C', out X' C' Q /\ Cong X' C' X C).
eapply l6_11_existence.
apply perp_distinct in H5.
spliter.
assumption.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
ex_and H8 C'.
exists C'.
unfold Cong_3 in *.
spliter.
assert (Cong A C A' C').
induction(eq_dec_points A X).
subst X.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst X'.
apply cong_symmetry.
assumption.
eapply l10_12.
3: apply H10.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H10.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;assumption.
apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.
assert (Cong B C B' C').
induction(eq_dec_points B X).
subst X.
apply cong_symmetry in H11.
apply cong_identity in H11.
subst X'.
apply cong_symmetry.
assumption.
eapply l10_12.
3: apply H11.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_comm.
apply H4.
apply col_permutation_4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H11.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
apply col_permutation_4.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.
repeat split.
assumption.
assumption.
assumption.
assert (T19 := (l9_19 A' B' C' Q X')).
assert (one_side A' B' C' Q <-> out X' C' Q /\ ~ Col A' B' C').
apply T19.
intro.
subst B'.
apply cong_identity in H1.
contradiction.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.
apply col_permutation_1.
apply out_col.
assumption.
apply cong_symmetry in H1.
destruct H14.
spliter.
assert (one_side A' B' C' Q).
apply H15.
split.
assumption.
intro.
apply H.
eapply l4_13.
apply H16.
unfold Cong_3.
repeat split.
assumption.
apply cong_symmetry.
assumption.
apply cong_symmetry.
assumption.
eapply one_side_transitivity.
apply H7.
apply one_side_symmetry.
assumption.
Qed.
End T10.