Library GeoCoq.Meta_theory.Models.hilbert_to_tarski

Tarski's betweenness is not strict:

Definition Bet A B C := BetH A B C A = B B = C.

Hilbert's congruence is 'defined' only for non degenerated segments, while Tarski's segment congruence allows the null segment.

Lemma betH_distincts : A B C, BetH A B C A B B C A C.
Proof.
intros.
assert(HH:= H).
assert(HP:= between_comm A B C H).
assert (HQ:=HP).
apply between_only_one in H.
apply between_only_one in HP.
split.
intro.
subst B.
contradiction.
split.
intro.
subst B.
contradiction.
intro.
subst C.
apply between_diff in HH.
tauto.
Qed.

Ltac line A B l Hdiff := let H:=fresh in (assert(H:= line_existence A B Hdiff); destruct H as [l]; spliter).

Lemma congH_perm : A B, AB CongH A B B A.
Proof.
intros.
line A B l H.
elim (cong_existence A B A B l); auto; intros B' H2.
spliter.
apply cong_pseudo_transitivity with A B'.
assumption.
apply cong_permr.
assumption.
Qed.

Lemma congH_refl : A B, AB CongH A B A B.
Proof.
intros.
apply cong_pseudo_transitivity with B A; auto using congH_perm.
Qed.

Lemma congH_sym : A B C D, AB CongH A B C D CongH C D A B.
intros.
assert(HH:= cong_pseudo_transitivity A B C D A B).
apply HH.
assumption.
apply congH_refl.
assumption.
Qed.

Global Instance Incid_morphism' : Proper(eq ==> EqL ==> iff) Incid.
Proof.
intro.
intro.
intro.
subst y.
intro.
intro.
intro.
split.
intro.
eapply (Incid_morphism _ x0).
assumption.
assumption.
intro.
eapply (Incid_morphism _ y).
assumption.
assert(HH:= EqL_Equiv).
destruct HH.
apply Equivalence_Symmetric.
assumption.
Qed.

Lemma plan' : A, B, C, ¬ ColH A B C.
Proof.
P0.
destruct (two_points_on_line l0) as [P1 [P2 [HP1 [HP2 HP3]]]].
P1.
P2.
assert (T:=plan).
intro.
apply T.
unfold ColH in H.
decompose [ex and] H.
assert (EqL l0 x).
apply line_uniqueness with P1 P2;auto.
rewrite H2 in ×.
intuition.
Qed.

Lemma colH_permut_231 : A B C, ColH A B C ColH B C A.
Proof.
intros.
unfold ColH in ×.
induction H.
x.
spliter.
repeat split; assumption.
Qed.

Lemma colH_permut_312 : A B C, ColH A B C ColH C A B.
Proof.
intros.
apply colH_permut_231 in H.
apply colH_permut_231 in H.
assumption.
Qed.

Lemma colH_permut_213 : A B C, ColH A B C ColH B A C.
Proof.
intros.
unfold ColH in ×.
induction H.
x.
spliter.
repeat split; assumption.
Qed.

Lemma colH_permut_132 : A B C, ColH A B C ColH A C B.
Proof.
intros.
apply colH_permut_312 in H.
apply colH_permut_213 in H.
assumption.
Qed.

Lemma colH_permut_321 : A B C, ColH A B C ColH C B A.
Proof.
intros.
apply colH_permut_312 in H.
apply colH_permut_132 in H.
assumption.
Qed.

Lemma other_point_exists : A: Point, B, A B.
Proof.
intros.
assert (T:=plan).
elim (two_points_on_line l0).
intros P.
intros.
destruct p.
induction(eq_dec_pointsH A x).
subst x.
P.
intuition.
x.
intuition.
Qed.

Lemma colH_trivial111 : A, ColH A A A.
Proof.
intros.
elim (other_point_exists A);intros.
assert (H1:= line_existence A x H).
decompose [ex and] H1.
x0.
intuition.
Qed.

Lemma colH_trivial112 : A B, ColH A A B.
Proof.
intros.
destruct (eq_dec_pointsH A B).
subst.
apply colH_trivial111.
assert (H1:= line_existence A B H).
decompose [ex and] H1.
x.
intuition.
Qed.

Lemma colH_trivial122 : A B, ColH A B B.
Proof.
intros.
destruct (eq_dec_pointsH A B).
subst.
apply colH_trivial111.
assert (H1:= line_existence A B H).
decompose [ex and] H1.
x.
intuition.
Qed.

Lemma colH_trivial121 : A B, ColH A B A.
Proof.
intros.
destruct (eq_dec_pointsH A B).
subst.
apply colH_trivial111.
assert (H1:= line_existence A B H).
decompose [ex and] H1.
x.
intuition.
Qed.

Hint Resolve colH_trivial121 colH_trivial122 colH_trivial112 colH_trivial111 colH_permut_231 colH_permut_312 colH_permut_321
             colH_permut_213 colH_permut_132 colH_permut_231 : col.

Ltac Col := auto 3 with col.

Ltac line_col A B C := match goal with
                          |H1:(Incid A ?l), H2:(Incid B ?l), H3:(Incid C ?l) |- _
                          ⇒ let HH := fresh in assert(ColH A B C) by (unfold ColH; l; repeat split; auto); auto
                       end.

Ltac col_line H l := assert(HH:=H); unfold ColH in HH; destruct HH as [l HH]; spliter.

Ltac lines_eq l m :=
match goal with
   | H0:(?X1 ?X2), H1:(Incid ?X1 l), H2:(Incid ?X1 m),
   H3:(Incid ?X2 l) , H4:(Incid ?X2 m) |- _let HH := fresh in assert(HH : EqL l m) by (apply (line_uniqueness X1 X2 l m);auto);
                                               rewrite <-HH in *;
                                               clean_duplicated_hyps
end.

Lemma colH_dec : A B C, ColH A B C ¬ColH A B C.
Proof.
intros.
induction(eq_dec_pointsH A B).
subst B.
left.
Col.
line A B l H.
induction(Incid_dec C l).
left.
line_col A B C.
right.
intro.
apply H2.
col_line H3 l00.
lines_eq l l00.
assumption.
Qed.

Lemma colH_trans : X Y A B C, X Y ColH X Y A ColH X Y B ColH X Y C ColH A B C.
Proof.
intros.
col_line H0 l.
col_line H1 m.
col_line H2 o.
lines_eq l m.
lines_eq l o.
line_col A B C.
Qed.

Global Instance Hilbert_is_a_Col_theory : (Col_theory Point ColH).
Proof.
exact (Build_Col_theory Point ColH colH_trivial112 colH_permut_231 colH_permut_132 colH_trans).
Defined.

Ltac ColHR :=
 let tpoint := constr:(Point) in
 let col := constr:(ColH) in
   Col_refl tpoint col.

Lemma ncolH_exists : A B, A B C, ¬ColH A B C.
Proof.
intros.
assert (HH:= plan').
destruct HH.
destruct H0.
destruct H0.
induction(colH_dec A B x).
induction(colH_dec A B x0).
induction(colH_dec A B x1).
apply False_ind.
apply H0.
ColHR.
x1.
assumption.
x0.
assumption.
x.
assumption.
Qed.

Lemma ncolH_distincts : A B C, ¬ColH A B C A B B C A C.
Proof.
intros.
repeat split;
intro;
apply H;
try subst B; Col.
subst C;Col.
Qed.

Definition Col := ColH.

Lemma betH_expand : A B C, BetH A B C BetH A B C A B B C A C ColH A B C.
Proof.
intros.
assert (HH0:= H).
apply betH_distincts in HH0.
spliter.
repeat split; auto.
apply between_col in H.
tauto.
Qed.

Ltac two_points l X Y := assert(_H := two_points_on_line l); destruct _H as [X _H]; destruct _H as [Y _H]; spliter.

Lemma inter_uniquenessH : A B A' B' X Y, A' B' ¬ColH A B A' ColH A B X ColH A B Y ColH A' B' X ColH A' B' Y X = Y.
Proof.
intros A B A' B' X Y HD.
intros.
assert(A B).
intro;subst B;apply H;Col.
induction(eq_dec_pointsH X Y).
assumption.
apply False_ind.
apply H.
ColHR.
Qed.

Lemma inter_incid_uniquenessH : P X Y l m,
  ¬Incid P l
  Incid P m Incid X l Incid Y l Incid X m Incid Y m
  X = Y.
Proof.
intros.
two_points l A B.
two_points m A' B'.

line_col A B X.
line_col A B Y.
line_col A' B' X.
line_col A' B' Y.

assert(¬ColH A B P).
intro.
apply H.
col_line H15 l00.
lines_eq l l00.
assumption.

induction(eq_dec_pointsH A' P).
subst P.

eapply(inter_uniquenessH A B A' B'); auto.

induction(eq_dec_pointsH P B').
subst P.
eapply(inter_uniquenessH A B B' A'); auto.
apply colH_permut_213.
assumption.
apply colH_permut_213.
assumption.

eapply(inter_uniquenessH A B P B'); auto.
unfold ColH.
m.
repeat split; auto.

unfold ColH.
m.
repeat split; auto.
Qed.

Lemma between_only_one' : A B C, BetH A B C ¬ BetH B C A ¬ BetH B A C.
Proof.
intros A B C HBet1; assert (HBet2 := between_comm _ _ _ HBet1).
split; apply between_only_one; auto.
Qed.

Lemma cut_comm : A B l, cut l A B cut l B A.
Proof.
intros.
unfold cut in ×.
spliter.
repeat split; auto.
destruct H1 as [I H1].
I.
spliter.
apply between_comm in H2.
split; auto.
Qed.

Lemma inner_pasch_aux : A B C P Q,
                            ¬Col B C P Bet A P C Bet B Q C
       X, Bet P X B Bet Q X A.
Proof.
intros.
unfold Bet in ×.
induction H0; induction H1.

elim (eq_dec_pointsH Q A);intros HQA.
subst.
exfalso.
apply H.
apply betH_expand in H1;spliter.
apply betH_expand in H0;spliter.
unfold Col.
ColHR.

line Q A l HQA.

induction(eq_dec_pointsH P A).
subst P.
A.
split; unfold Bet.
right; left.
auto.
right; right.
auto.

induction(eq_dec_pointsH Q C).
subst Q.
P.
split;
unfold Bet in ×.
right; left; auto.

left.
apply between_comm.
assumption.

assert(HI:¬Incid P l).
intro.
apply H.
apply between_col in H0.
apply between_col in H1.
spliter.
line_col A P Q.
assert(Col P C Q).
eapply (colH_trans A P); Col.
eapply (colH_trans Q C); Col.

induction(eq_dec_pointsH B Q).
subst Q.
B.

split;
 right.
right; auto.
left; auto.

induction(eq_dec_pointsH A C).
subst C.
apply False_ind.
apply betH_distincts in H0.
solve [intuition].

assert(¬Incid B l).
intro.
line_col A B Q.
assert(Col A B C).
apply between_col in H0.
apply between_col in H1.
spliter.
apply(colH_trans B Q);
Col.
apply between_col in H0.
apply between_col in H1.
spliter.
apply H.

apply (colH_trans A C); Col.

assert(¬Incid C l).
intro.
line_col A C Q.
assert(Col A B C).
apply between_col in H1.
spliter.
apply(colH_trans C Q);
Col.
apply H.
apply between_col in H0.
apply between_col in H1.
spliter.
apply (colH_trans A C);Col.

assert(cut l B C).
unfold cut.
repeat split; auto.
Q.
split; auto.

assert(PH:=pasch B C P l H HI H10).
induction PH.

unfold cut in H11.
spliter.
destruct H13 as [X HX].
X.
spliter.
split.
left.
apply between_comm.
assumption.
induction(eq_dec_pointsH A X).
subst X.
right; right; auto.
assert(A Q).
intro.
subst Q.
apply between_col in H0.
apply between_col in H1.
spliter.
apply H.
unfold Col.
apply (colH_trans A C);Col.
assert(P C).
  intro.
  subst P.
  apply H.
  unfold Col.
  Col.
assert(A B).
  intro.
  subst B.
  apply between_col in H0.
  spliter.
  apply H.
  unfold Col.
  Col.
assert(X Q).
intro.
subst X.
apply H.
apply between_col in H1.
apply between_col in H14.
spliter.
apply (colH_trans B Q); Col.
assert(ColH A X Q).
unfold ColH.
l.
split; auto.
assert(HN:¬ ColH A C Q).
intro.
apply H9.
col_line H21 l00.

lines_eq l l00.

assumption.
assert (HPB : PB).
apply ncolH_distincts in H.
intuition.
line P B m HPB.
assert(¬ Incid Q m).
intro.
apply H.
unfold Col.

unfold ColH.
m.
repeat split; try assumption.
apply between_col in H1.
spliter.
col_line H1 m0.
lines_eq m m0.
assumption.

assert(¬ColH A B P).
intro.
apply H.
apply(colH_trans A P); Col.
apply between_col in H0.
tauto.

assert(cut m A C).
unfold cut.
split.
intro.
apply H24.
unfold ColH.
m.
repeat split; auto.
split.
intro.
apply H.
unfold Col.
unfold ColH.
m.
repeat split; auto.
P.
split; auto.

assert(HH:= pasch A C Q m HN H23 H25).
induction HH.
unfold cut in H26.
spliter.
destruct H28 as [Y H28].
spliter.

assert(X=Y).
apply(inter_incid_uniquenessH B X Y l m); auto.
apply between_col in H29.
spliter.
unfold ColH in H29.
destruct H29 as [l0 H29].
spliter.
lines_eq l0 l.
assumption.
apply between_col in H14.
spliter.
col_line H14 m0.
lines_eq m m0.
assumption.
subst Y.
left.
apply between_comm.
assumption.

unfold cut in H26.
spliter.

destruct H28 as [I H28].
spliter.
assert(ColH C I Q).
apply between_col in H29.
tauto.
col_line H30 o.
assert(¬Incid C m).
intro.
apply H.
unfold Col.
unfold ColH.
m.
repeat split; auto.

assert(Incid B o).
apply between_col in H1.
spliter.
col_line H1 n0.
lines_eq o n0.
assumption.

assert(HH:= inter_incid_uniquenessH C I B m o H34 H31 H28 H22 H32 H35).
subst I.
apply False_ind.
apply between_only_one' in H1.
spliter.
apply H36.
apply between_comm.
assumption.

unfold cut in H11.
spliter.
destruct H13 as [I H13].
spliter.
assert(A = I).

line A C s H7.

apply (inter_incid_uniquenessH Q A I s l); auto.
intro.

assert( A Q).
intro.
subst Q.
apply between_col in H1.
spliter.
apply H.
unfold Col.
apply between_col in H0.
spliter.
apply (colH_trans A C); Col.

lines_eq l s.
unfold cut in H10.
spliter.
contradiction.
apply between_col in H14.
spliter.
apply between_col in H0.
spliter.
unfold ColH in H0.
destruct H0 as [s0 H0].
spliter.
lines_eq s s0.

col_line H14 s1.
apply ncolH_distincts in H;spliter.
lines_eq s s1.
assumption.
subst I.
apply between_only_one in H14.
spliter.

contradiction.

induction H1.
subst Q.
B.
split.
right;right; auto.
right;left;auto.
subst Q.
P.
split.
right;left; auto.
left.
apply between_comm.
assumption;
subst P.
induction H0.
subst P.
A.
split.
right;left; auto.
right; right; auto.
subst P.
apply False_ind.
apply H.
unfold Col.
Col.
induction H0.
subst P.
A.
split.
right;left; auto.
right; right; auto.
subst P.
apply False_ind.
apply H.
unfold Col.
Col.
Qed.

Lemma betH_trans1 : A B C D, BetH A B C BetH B C D BetH A C D.
Proof.
intros.
assert(HH0 := H).
assert(HH1:= H0).
apply betH_distincts in HH0.
apply betH_distincts in HH1.
spliter.
clean_duplicated_hyps.
assert(HH:=ncolH_exists A C H6).
destruct HH as [E HE].
assert(C E).
apply ncolH_distincts in HE.
tauto.
assert(HF:=between_out C E H1).
destruct HF as [F HF].
assert(HHF:=HF).
apply betH_distincts in HHF.
spliter.

assert(ColH A B C).
apply between_col in H.
tauto.
assert(ColH B C D).
apply between_col in H0.
tauto.
assert(ColH C E F).
apply between_col in HF.
tauto.

assert(¬ColH F C B).
intro.
assert(ColH C E B).
apply (colH_trans C F); Col.
apply HE.
apply (colH_trans B C); Col.

assert( X : Point, Bet B X F Bet E X A).
apply(inner_pasch_aux A F C B E H13).
unfold Bet.
left; assumption.
unfold Bet.
left; apply between_comm; assumption.
destruct H14 as [G H14].
spliter.

induction H14.
induction H15.
assert(HH15:=H14).
apply between_col in HH15.
assert(HH16:=H15).
apply between_col in HH16.
spliter.

assert(¬ColH D B G).
intro.
assert(ColH B D F).
apply (colH_trans B G); Col.
intro.
subst G.
apply HE.
apply(colH_trans A B); Col.
apply H13.
apply(colH_trans B D); Col.

line C E m H1.


assert(~(cut m A G cut m B G)).
intro.
induction H19.
unfold cut in H19.
spliter.
ex_and H21 E'.
assert(E = E').
apply (inter_uniquenessH A G C F E E'); Col.
intro.
assert(ColH B C G).
apply (colH_trans A C); Col.
apply H16.
apply (colH_trans B C); Col.
unfold ColH in H12.
apply between_col in H22.
spliter.
Col.
ex_and H12 m0.
lines_eq m m0.
line_col C F E'.
subst E'.
apply between_only_one in H22.
tauto.
unfold cut in H19.
spliter.
ex_and H21 F'.
assert(F = F').
apply betH_distincts in H14.
spliter.
apply (inter_uniquenessH C E B G); Col.
intro.
apply HE.
apply (colH_trans B C); Col.
line_col C E F'.
apply between_col in H22.
spliter; Col.
subst F'.
apply between_only_one in H22.
spliter.
apply between_comm in H14.
contradiction.

assert(¬ ColH B D G ).
intro.
apply H16. Col.

assert(¬Incid G m).
spliter.
intro.
assert(ColH C E G).
unfold ColH.
m; split; auto.
apply betH_distincts in H15.
spliter.
apply HE.
apply (colH_trans E G); Col.

assert(cut m D B).
unfold cut.

split.

intro.
assert(ColH A C D).
apply(colH_trans B C); Col.
apply HE.
apply(colH_trans C D); Col.
line_col C D E.

split.
intro.
apply HE.
apply(colH_trans B C); Col.
line_col B C E.
C.
split; auto.
apply between_comm.
assumption.
apply cut_comm in H22.

assert(HP:= pasch B D G m H20 H21 H22).
induction HP.

apply False_ind.
apply H19.
right.
assumption.
unfold cut in H23.
spliter.
destruct H25 as [HX H25].
spliter.

assert(¬ ColH G D A).
intro.
assert(ColH A B D).
apply (colH_trans B C); Col.
apply H20.
apply (colH_trans A D); Col.
intro.
subst D.
apply between_only_one' in H0.
spliter.
apply between_comm in H.
contradiction.

assert(¬Incid A m).
intro.
apply HE.
line_col A C E.

assert(cut m G D).
unfold cut.
repeat split; auto.
HX.
split; auto.
apply between_comm.
assumption.

assert(HP:=pasch G D A m H27 H28 H29).
induction HP.
apply False_ind.
apply H19.
left.
apply cut_comm.
assumption.
unfold cut in H30.
spliter.
ex_and H32 C'.

assert(C'= C).
apply(inter_uniquenessH A D E F); Col.
intro.
apply HE.
assert(Col A C D).
apply (colH_trans B C); Col.
apply (colH_trans A D); Col.
intro.
subst D.
apply H27.
Col.
apply between_col in H33;
spliter.
Col.
apply (colH_trans B C); Col.
unfold ColH in H12.
ex_and H12 m0.
lines_eq m m0.
line_col E F C'.
subst C'.
apply between_comm.
assumption.
induction H15.
subst G.
apply False_ind.
apply between_col in H14.
spliter.
apply H13.
apply (colH_trans E F); Col.
subst G.
apply False_ind.
apply between_col in H14.
spliter.
apply H13.
apply (colH_trans A B); Col.
induction H14.
induction H15.
subst G.
apply False_ind.
apply between_col in H15.
spliter.
apply HE.
apply(colH_trans A B); Col.
subst G.
induction H15.
subst E.
apply False_ind.
apply H13.
Col.
subst B; tauto.
subst G.
induction H15.
apply between_col in H14.
spliter.
apply False_ind.
apply HE.
apply (colH_trans E F); Col.
induction H14.
subst F.
tauto.
subst F.
apply False_ind.
apply H13.
Col.
Qed.

Lemma betH_trans2 : A B C D, BetH A B C BetH B C D BetH A B D.
Proof.
intros.
apply between_comm.
apply between_comm in H.
apply between_comm in H0.
apply (betH_trans1 D C B A); auto.
Qed.

Lemma betH_trans : A B C D, BetH A B C BetH B C D BetH A B D BetH A C D.
Proof.
intros.
split.
apply (betH_trans2 A B C D); auto.
apply (betH_trans1 A B C D); auto.
Qed.

Lemma not_cut3 : A B C l,¬Incid A l ¬ColH A B C ¬cut l A B ¬cut l A C ¬cut l B C.
Proof.
intros.
intro.
assert(¬ColH B C A).
intro.
apply H0;
Col.
assert(HH:= pasch B C A l H4 H H3).
induction HH.
apply cut_comm in H5.
contradiction.
apply cut_comm in H5.
contradiction.
Qed.

Lemma betH_trans0 : A B C D, BetH A B C BetH A C D BetH B C D BetH A B D.
Proof.
intros.
apply betH_expand in H.
apply betH_expand in H0.
spliter.
clean_duplicated_hyps.
assert(HH:=ncolH_exists A B H5).
destruct HH as [G HE].
assert(B G).
apply ncolH_distincts in HE.
tauto.
assert(HF:=between_out B G H1).
ex_and HF F.
apply betH_expand in H9.
spliter.

elim (eq_dec_pointsH C F).
intros HCF.
subst.
exfalso.
apply HE.
apply (colH_trans B F);Col.
intro HCF.

line C F l HCF.

assert(¬cut l A B).
intro.
unfold cut in H16.
spliter.
ex_and H18 X.
assert(X=C).
apply (inter_uniquenessH A B F C); Col.

intro.
apply HE.
apply(colH_trans B F); Col.
apply between_col in H19.
spliter; Col.
line_col F C X.
subst X.
apply between_only_one in H19.
spliter.
apply between_comm in H.
contradiction.

assert(¬cut l B G).
intro.
unfold cut in H17.
spliter.
ex_and H19 X.
apply betH_expand in H20.
spliter.
assert(ColH B X F).
apply (colH_trans B G); Col.
col_line H25 l00.
assert(X F).
intro.
subst X.
apply between_only_one in H20.
spliter.
apply between_comm in H9.
contradiction.
lines_eq l l00.
contradiction.
assert(¬cut l A G).
apply (not_cut3 B).
intro.
assert(ColH B C G).
apply (colH_trans B F);Col.
line_col B F C.
apply HE.
apply (colH_trans B C); Col.
intro.
apply HE; Col.
intro.
apply cut_comm in H18.
contradiction.
intro.
contradiction.

assert(cut l A G cut l D G).
apply(pasch A D G l).
intro.
apply HE.
apply(colH_trans A D); Col.
apply (colH_trans A C) ; Col.
intro.
assert(ColH B C G).
apply (colH_trans G F); Col.
line_col G F C.
apply HE.
apply (colH_trans B C); Col.
unfold cut.
repeat split.
intro.
assert(ColH A C F).
line_col A C F.
assert(ColH A B F).
apply (colH_trans A C); Col.
apply HE.
apply (colH_trans B F); Col.
intro.
assert(ColH C D F).
line_col C D F.
assert(ColH A C F).
apply (colH_trans C D); Col.
assert(ColH A B F).
apply (colH_trans A C); Col.
apply HE.
apply (colH_trans B F); Col.
C.
split; auto.
induction H19.
contradiction.

assert(¬ ColH D G B).
intro.
assert(ColH A B D).
apply (colH_trans A C); Col.
apply HE.
apply (colH_trans B D); Col.
intro.
subst D.
apply between_only_one in H0.
spliter.
apply between_comm in H.
contradiction.
assert(¬ Incid B l).
intro.
assert(ColH B C G).
apply (colH_trans B F); Col.
line_col B F C.
apply HE.
apply (colH_trans B C); Col.

assert(HH:=pasch D G B l H20 H21 H19).
induction HH.
unfold cut in H22.
spliter.
ex_and H24 C'.
assert(C = C').
assert(ColH C C' F).
line_col C C' F.
apply (inter_uniquenessH A B F C); Col.
intro.
apply HE.
apply (colH_trans B F); Col.
apply betH_expand in H25.
spliter.
apply (colH_trans B D); Col.
apply (colH_trans A C); Col.
subst C'.
assert(BetH B C D).
apply between_comm.
assumption.
split; auto.
assert(HH:=betH_trans A B C D H H26).
tauto.
apply cut_comm in H22.
contradiction.
Qed.

Lemma betH_outH2__betH: A B C A' C',
 BetH A B C
 outH B C C'
 outH B A A'
 BetH A' B C'.
Proof.
intros.
destruct H0.
 - destruct H1.
   assert (BetH A B C')
     by (apply (betH_trans A B C C');auto).
   apply between_comm.
   apply (betH_trans C' B A A'); auto using between_comm.
   destruct H1.

   assert (BetH C B A') by
      (apply between_comm;
      apply (betH_trans0 A A' B C);auto using between_comm).
   apply (betH_trans A' B C C');auto using between_comm.
   spliter;subst.
    apply between_comm;
   apply (betH_trans C' C B A');auto using between_comm.
 - destruct H0.
   destruct H1.
   assert (BetH A B C').
    apply between_comm;
    apply (betH_trans0 C C' B A);auto using between_comm.
   apply between_comm; apply (betH_trans C' B A A');auto using between_comm.
   destruct H1.
   assert (BetH A B C').
     apply between_comm; apply (betH_trans0 C C' B A);auto using between_comm.
   apply (betH_trans0 A A' B C');auto using between_comm.
   spliter;subst.
   apply between_comm;apply (betH_trans0 C C' B A');auto using between_comm.
   spliter;subst.
   destruct H1.
   apply (betH_trans A' A B C');auto using between_comm.
   destruct H1.
   apply (betH_trans0 A A' B C');auto using between_comm.
   spliter;subst.
   assumption.
Qed.

Lemma cong_existence' : A B l M,
  A B
  Incid M l
   A' B', Incid A' l Incid B' l BetH A' M B' CongH M A' A B CongH M B' A B.
Proof.
intros A B l M HAB HInM.
assert (H : P, Incid P l M P).
  {
  destruct (two_points_on_line l) as [P1 [P2 [HP2 [HP1 HP1P2]]]].
  elim (eq_dec_pointsH M P1); intro HMP1; try subst P1; [ P2; auto|].
  elim (eq_dec_pointsH M P2); intro HMP2; try subst P2; P1; auto.
  }
destruct H as [P [HInP HMP]].
destruct (between_out P M) as [P' HP']; auto.
destruct (cong_existence A B M P l) as [A' [HInA' [HoutA' HCongA']]]; auto.
destruct (cong_existence A B M P' l) as [B' [HInB' [HoutB' HCongB']]]; auto;
[apply betH_distincts in HP'; tauto|apply between_col in HP'|
  A', B'; repeat split; auto; apply betH_outH2__betH with P P'; auto].
destruct HP' as [l' [HIn1 [HIn2 HIn3]]]; apply Incid_morphism with l'; auto.
apply line_uniqueness with M P; auto.
Qed.

Definition Cong A B C D := (CongH A B C D A B C D) (A = B C = D).

Lemma betH_to_bet : A B C , BetH A B C Bet A B C A B B C A C.
Proof.
intros.
assert(HH:= betH_distincts A B C H).
induction HH.
split.
unfold Bet.
left.
assumption.
spliter.
repeat split; assumption.
Qed.

Lemma betH_line : A B C, BetH A B C
   l, Incid A l Incid B l Incid C l.
Proof.
intros.
apply between_col in H.
assumption.
Qed.


Lemma bet_identity : A B, Bet A B A A = B.
Proof.
intros.
unfold Bet in H.
induction H.
apply False_ind.
apply betH_distincts in H.
spliter.
tauto.
induction H.
tauto.
apply sym_equal.
tauto.
Qed.


Lemma morph : l m, EqL l m ( A, Incid A l Incid A m).
Proof.
intros.
split.
intro.
rewrite <-H.
assumption.
intro.
rewrite H.
assumption.
Qed.

Lemma betH_colH : A B C, BetH A B C ColH A B C A B B C A C.
Proof.
intros.
split.
apply between_col in H.
tauto.
apply betH_distincts in H.
tauto.
Qed.

Lemma point3_online_exists : A B l, Incid A l Incid B l C, Incid C l C A C B.
Proof.
intros.
induction(eq_dec_pointsH A B).
subst B.
two_points l A0 B0.
induction(eq_dec_pointsH A A0).
subst A0.
B0.
split; auto.
A0.
split; auto.
assert(HH:= between_out A B H1).
destruct HH as [C HH].
apply betH_colH in HH.
spliter.
C.
unfold ColH in H3.
destruct H2 as [m H2].
spliter.
lines_eq l m.
split; auto.
Qed.

Lemma not_betH121 : A B, ¬BetH A B A.
Proof.
intros.
intro.
apply betH_colH in H.
tauto.
Qed.

Ltac out_exists A B X := try match goal with |H : A B |- _
                                 ⇒ assert(HH:=between_out A B H);auto; destruct HH as [X]
                              end.

Ltac not_on_line A B X := try match goal with |H : A B |- _
                                 ⇒ assert(HH:=ncolH_exists A B H);auto; destruct HH as [X]
                              end.


Lemma cong_identity : A B C , Cong A B C C A = B.
Proof.
intros.
unfold Cong in H.
induction H.
spliter;
tauto.
tauto.
Qed.


Lemma cong_inner_transitivity : A B C D E F, Cong A B C D Cong A B E F Cong C D E F.
Proof.
intros.
unfold Cong in ×.
induction H.
induction H0.
spliter.
left.
repeat split; auto.
apply (cong_pseudo_transitivity A B); auto.
spliter.
contradiction.
induction H0.
spliter.
contradiction.
right.
tauto.
Qed.

Lemma bet_colH : A B C, Bet A B C ColH A B C.
Proof.
intros.
unfold Bet in H.
induction H.
apply between_col in H.
spliter.
unfold Col in H.
assumption.
induction H;
subst B; Col.
Qed.

Lemma other_point_on_line : A l, Incid A l B, A B Incid B l.
Proof.
intros.
assert(HH:= two_points_on_line l).
destruct HH as [X HH].
destruct HH as [Y HH].
spliter.
induction(eq_dec_pointsH A X).
Y.
subst X.
split; auto.
X.
split; auto.
Qed.

Lemma bet_disjoint : A B C, BetH A B C disjoint A B B C.
intros.
unfold disjoint.
intro.
ex_and H0 P.
assert(HP:= betH_trans0 A P B C H0 H).
spliter.
apply between_only_one' in H1.
spliter.
contradiction.
Qed.

Lemma addition_betH : A B C A' B' C',
  BetH A B C BetH A' B' C'
  CongH A B A' B' CongH B C B' C'
  CongH A C A' C'.
Proof.
intros.
apply addition with B B';auto using bet_disjoint, between_col.
Qed.

Lemma outH_trivial : A B, AB outH A B B.
Proof.
intros.
unfold outH.
intuition.
Qed.

Lemma same_side_refl : l A,
 ¬ Incid A l
 same_side A A l.
Proof.
intros.
unfold same_side.
unfold cut.
destruct (two_points_on_line l).
destruct s.
spliter.
destruct (between_out A x).
intro;subst. intuition.
x1.
repeat split;try assumption.
intro.
apply betH_expand in H3.
spliter.
destruct H8.
spliter.
assert (EqL x2 l).
apply line_uniqueness with x x1;try assumption.
apply H.
rewrite H11 in H8;auto.
x;auto.
 intro.
apply betH_expand in H3.
spliter.
destruct H8.
spliter.
assert (EqL x2 l).
apply line_uniqueness with x x1;try assumption.
apply H.
rewrite H11 in H8;auto.
x;auto.
Qed.

Lemma same_side_prime_refl: A B C,
 ¬ ColH A B C same_side' C C A B.
Proof.
intros.
unfold same_side'.
split.
apply ncolH_distincts in H;intuition.
intros.
apply same_side_refl.
intro.
apply H.
l;auto.
Qed.

Hint Resolve between_comm betH_trans0 betH_trans1 : bet.

Ltac Bet := auto 3 with bet.

Lemma outH_expand: A B C,
  outH A B C outH A B C ColH A B C AC AB.
Proof.
intros.
split; auto.
unfold outH in ×.
decompose [or] H.
apply betH_expand in H0;intuition.
apply betH_expand in H1;intuition.
destruct H1.
subst.
split.
Col.
auto.
Qed.

Lemma construction_uniqueness : A B D E,
  BetH A B D BetH A B E CongH B D B E D = E.
Proof.
intros A B D E HBet1 HBet2 HCong.
assert (HD1 : A B) by (apply betH_expand in HBet1; spliter; auto).
destruct (ncolH_exists _ _ HD1) as [C HNC].
assert (HConga : CongaH A C D A C E).
  {
  assert (HD2 := between_diff _ _ _ HBet1).
  assert (HD3 := between_diff _ _ _ HBet2).
  assert (HC1 := between_col _ _ _ HBet1).
  assert (HC2 := between_col _ _ _ HBet2).
  apply cong_5; try apply congH_refl; try apply addition_betH with B B;
  try apply congH_refl; auto; try (intro; subst; Col); try (apply HNC; ColHR).
  apply congaH_outH_congaH with C B C B; try apply outH_trivial; try left; auto;
  try apply conga_refl; try intro; subst; apply HNC; Col.
  }
assert (Hout : outH C D E).
  {
  assert (HD2 := between_diff _ _ _ HBet1).
  assert (HC := between_col _ _ _ HBet1).
  apply (hcong_4_uniqueness A C D C D A D E); try apply conga_refl;
  try apply same_side_prime_refl; auto; try (intro; apply HNC; ColHR).
  destruct (between_out B A) as [F HBet3]; auto.
  split; [intro; subst; Col|intros l HI1 HI2; F; split].

    {
    split; [intro; assert (ColH A C D) by ( l; auto); apply HNC; ColHR|].
    apply betH_expand in HBet3; spliter.
    split; [intro; assert (ColH A C F) by ( l; auto); apply HNC; ColHR|].
     A; split; eauto with bet.
    }

    {
    apply betH_expand in HBet2; spliter.
    split; [intro; assert (ColH A C E) by ( l; auto); apply HNC; ColHR|].
    apply betH_expand in HBet3; spliter.
    split; [intro; assert (ColH A C F) by ( l; auto); apply HNC; ColHR|].
     A; split; eauto with bet.
    }
  }
apply betH_expand in HBet1; apply betH_expand in HBet2;
apply outH_expand in Hout; spliter; apply inter_uniquenessH with A B C D; Col.
Qed.

Lemma out_distinct : A B C, outH A B C A B A C.
Proof.
intros.
unfold outH in H.
induction H.
apply betH_distincts in H.
intuition.
induction H.
apply betH_distincts in H.
intuition.
spliter.
subst C.
intuition.
Qed.

Lemma out_same_side : A B C l, Incid A l ¬Incid B l outH A B C same_side B C l.
Proof.
intros.
assert(B A).
apply out_distinct in H1.
intuition.
assert(HH:= between_out B A H2).
ex_and HH P.
P.
assert(¬Incid P l).
intro.
apply betH_expand in H3.
spliter.
col_line H8 ll.
lines_eq l ll.
contradiction.
split.
unfold cut.
repeat split; auto.
A.
split; auto.
repeat split; auto.
intro.
unfold outH in H1.
induction H1.

apply betH_expand in H1.
spliter.
col_line H9 m.
lines_eq l m.
contradiction.
induction H1.
apply betH_expand in H1.
spliter.
col_line H9 m.
lines_eq l m.
contradiction.
spliter.
subst C.
contradiction.
A.
split; auto.

unfold outH in H1.
induction H1.

assert(BetH P A C BetH P B C).
apply(betH_trans P A B C); Bet.
spliter.
Bet.
induction H1.
assert(BetH C A P BetH B C P).
apply(betH_trans0 B C A P); Bet.
tauto.
spliter.
subst C.
auto.
Qed.

Lemma between_one : A B C,
  A B A C B C ColH A B C
  BetH A B C BetH B C A BetH B A C.
Proof.
intros A B C HD1 HD2 HD3 HC.
destruct (ncolH_exists _ _ HD2) as [D HNC1].
assert (HD4 : B D) by (intro; subst; apply HNC1; Col).
destruct (between_out _ _ HD4) as [G HBet1].
assert (HD5 : A D) by (intro; subst; Col); line A D lAD HD5.
assert (HD6 : C D) by (intro; subst; Col); line C D lCD HD6.
assert (HNC2 : ¬ ColH B G C)
  by (intro; apply betH_expand in HBet1; spliter; apply HNC1; ColHR).
assert (HNC3 : ¬ ColH B G A)
  by (intro; apply betH_expand in HBet1; spliter; apply HNC1; ColHR).
assert (HNI1 : ¬ Incid C lAD) by (intro; apply HNC1; lAD; auto).
assert (HNI2 : ¬ Incid A lCD) by (intro; apply HNC1; lCD; auto).
assert (HCut1 : cut lAD B G).
  {
  apply betH_expand in HBet1; spliter.
  split; [intro; assert (ColH A B D) by ( lAD; auto); apply HNC1; ColHR|].
  split; [intro; assert (ColH A D G) by ( lAD; auto); apply HNC1; ColHR|].
   D; auto.
  }
assert (HCut2 : cut lCD B G).
  {
  apply betH_expand in HBet1; spliter.
  split; [intro; assert (ColH B C D) by ( lCD; auto); apply HNC1; ColHR|].
  split; [intro; assert (ColH C D G) by ( lCD; auto); apply HNC1; ColHR|].
   D; auto.
  }
elim (pasch _ _ _ _ HNC2 HNI1 HCut1); intro HCut3;
elim (pasch _ _ _ _ HNC3 HNI2 HCut2); intro HCut4.

  {
  destruct HCut3 as [_ [_ [I [HI3 HBet2]]]].
  elim (eq_dec_pointsH A I); intro HD7; [subst; right; right; auto|].
  assert (I = A); [|subst; right; right; auto].
  apply betH_expand in HBet2; spliter.
  assert (ColH A D I) by ( lAD; auto).
  apply inter_uniquenessH with B C D A; try (intro; apply HNC1); Col; ColHR.
  }

  {
  destruct HCut3 as [_ [_ [I [HI3 HBet2]]]].
  elim (eq_dec_pointsH A I); intro HD7; [subst; right; right; auto|].
  assert (I = A); [|subst; right; right; auto].
  apply betH_expand in HBet2; spliter.
  assert (ColH A D I) by ( lAD; auto).
  apply inter_uniquenessH with B C D A; try (intro; apply HNC1); Col; ColHR.
  }

  {
  destruct HCut4 as [_ [_ [I [HI3 HBet2]]]].
  elim (eq_dec_pointsH C I); intro HD7; [subst; right; left; auto|].
  assert (I = C); [|subst; right; left; auto].
  apply betH_expand in HBet2; spliter.
  assert (ColH C D I) by ( lCD; auto).
  apply inter_uniquenessH with A B D C; try (intro; apply HNC1); Col; ColHR.
  }

  {
  destruct HCut3 as [_ [_ [E [HI3 HBet2]]]].
  destruct HCut4 as [_ [_ [F [HI4 HBet3]]]].
  assert (HNC4 : ¬ ColH A G E).
    {
    intro; apply betH_expand in HBet1; apply betH_expand in HBet2; spliter.
    apply HNC1; ColHR.
    }
  assert (HD7 : C F); [|line C F lCF HD7].
    {
    apply betH_expand in HBet2; apply betH_expand in HBet3; spliter.
    intro; subst; apply HNC4; ColHR.
    }
  assert (HNI3 : ¬ Incid E lCF).
    {
    apply betH_expand in HBet1; apply betH_expand in HBet2;
    apply betH_expand in HBet3; spliter.
    intro; assert (ColH C E F) by ( lCF; auto); apply HNC1; ColHR.
    }
  assert (HCut3 : cut lCF A G).
    {
    apply betH_expand in HBet1; apply betH_expand in HBet2;
    apply betH_expand in HBet3; spliter.
    split; [intro; assert (ColH A C F) by ( lCF; auto); apply HNC1; ColHR|].
    split; [intro; assert (ColH C F G) by ( lCF; auto); apply HNC1; ColHR|].
     F; auto; split; try apply between_comm; auto.
    }
  elim (pasch _ _ _ _ HNC4 HNI3 HCut3); intro HCut4.

    {
    destruct HCut4 as [_ [_ [I [HI5 HBet4]]]].
    assert (I = D); [|subst].
      {
      apply betH_expand in HBet4; spliter.
      apply inter_uniquenessH with C D A E; try intro; subst; Col;
      [| lAD]; auto.
      assert (ColH C D F) by ( lCD; auto).
      assert (ColH C F I) by ( lCF; auto); ColHR.
      }
    assert (HNC5 : ¬ ColH A E C)
      by (intro; apply betH_expand in HBet4; spliter; apply HNC1; ColHR).
    assert (HD8 : B D) by (intro; subst; apply HNC1; Col).
    line B D lBD HD8; assert (HNI4 : ¬ Incid C lBD)
      by (intro; assert (ColH B C D) by ( lBD; auto); apply HNC1; ColHR).
    assert (HCut4 : cut lBD A E).
      {
      apply betH_expand in HBet4; spliter.
      split; [intro; assert (ColH A B D) by ( lBD; auto); apply HNC1; ColHR|].
      split; [intro; assert (ColH B D E) by ( lBD; auto); apply HNC1; ColHR|].
       D; auto.
      }
    elim (pasch _ _ _ _ HNC5 HNI4 HCut4); intro HCut5.

      {
      destruct HCut5 as [_ [_ [I [HI6 HBet5]]]].
      assert (I = B); [|subst; left; auto].
      apply betH_expand in HBet5; spliter.
      apply inter_uniquenessH with A C D B; Col; lBD; auto.
      }

      {
      destruct HCut5 as [_ [_ [I [HI6 HBet5]]]].
      assert (I = G); [|subst].
        {
        apply betH_expand in HBet1; apply betH_expand in HBet2;
        apply betH_expand in HBet5; spliter.
        apply inter_uniquenessH with D B C E; Col; try lBD; auto.
        intro; apply HNC1; ColHR.
        }
      apply between_only_one' in HBet5; spliter; intuition.
      }
    }

    {
    destruct HCut4 as [_ [_ [I [HI5 HBet4]]]].
    assert (I = C); [|subst].
      {
      apply betH_expand in HBet1; apply betH_expand in HBet2;
      apply betH_expand in HBet3; apply betH_expand in HBet4; spliter.
      apply inter_uniquenessH with G E F C; Col; try lCF; auto.
      intro; apply HNC4; ColHR.
      }
    apply between_only_one' in HBet4; spliter; intuition.
    }
  }
Qed.

Lemma betH_dec : A B C, A B B C A C BetH A B C ¬ BetH A B C.
Proof.
intros.
induction(colH_dec A B C).
assert(HH:=between_one A B C H H1 H0 H2).
induction HH.
left; assumption.
induction H3.
apply between_only_one' in H3.
spliter.
right.
intro.
apply H4.
apply between_comm.
assumption.
apply between_only_one' in H3.
spliter.
right.
assumption.
right.
intro.
apply H2.
apply between_col in H3.
spliter.
assumption.
Qed.

Lemma cut2_not_cut : A B C l, ¬ColH A B C cut l A B cut l A C ¬cut l B C.
intros.
unfold cut in ×.
intro.
spliter.
destruct H8 as [AB Hab].
destruct H6 as [AC Hac].
destruct H4 as [BC Hbc].
spliter.
assert(ColH A AB B ColH A AC C ColH B BC C).
repeat split.
apply between_col in H11.
tauto.
apply between_col in H9.
tauto.
apply between_col in H6.
tauto.
spliter.
assert(ColH AB AC BC).
line_col AB AC BC.

assert(AB AC AB BC AC BC).
{
apply betH_distincts in H11.
apply betH_distincts in H9.
apply betH_distincts in H6.
spliter.
repeat split;
intro;
apply H.
subst AC.
apply(colH_trans A AB); Col.
subst BC.
apply(colH_trans B AB); Col.
subst BC.
apply(colH_trans C AC); Col.
}
spliter.

assert(HH:=between_one AB AC BC H16 H17 H18 H15).
assert(HH12:= H11).
assert(HH10:= H9).
assert(HH7:=H6).
apply betH_distincts in HH12.
apply betH_distincts in HH10.
apply betH_distincts in HH7.
spliter.

induction HH.

line A C m H24.

assert(¬ ColH AB BC B).
 { intro.
   apply H.
   assert(Col A B BC).
   apply(colH_trans B AB); Col.
   apply(colH_trans B BC); Col.
 }

assert(¬ Incid B m).
intro.
apply H.
line_col A B C.

assert(cut m AB BC).
unfold cut.
repeat split.
intro.
apply H.
apply(colH_trans A AB); Col.
line_col A AB C.

intro.
apply H.
line_col A C BC.
apply(colH_trans C BC); Col.

AC.

split.
col_line H13 m0.
lines_eq m m0.
assumption.
assumption.

assert(HH:= pasch AB BC B m H31 H32 H33).

induction HH.
unfold cut in H34.
spliter.
destruct H36 as [I H36].
spliter.

assert(HH37:= H37).
apply between_col in HH37.
spliter.
apply H.
assert(ColH A I B).
apply(colH_trans B AB); Col.
assert(ColH A I C).
line_col A I C.
apply (colH_trans A I); Col.
intro.
subst I.
apply between_only_one' in H37.
tauto.

unfold cut in H34.
spliter.
destruct H36 as [C' H36].
spliter.

assert(HH38:=H37).
apply between_col in HH38.
spliter.
assert(ColH B C C').
apply(colH_trans B BC); Col.
assert(C C').
intro.
subst C'.
unfold cut in H33.
spliter.
destruct H40 as [I H42].
spliter.
assert(I = AC).
apply(inter_uniquenessH A C AB BC); Col.
intro.
apply H.
apply (colH_trans A AB); Col.
line_col A C I.
apply between_col in H41.
spliter.
Col.
subst I.
clean_duplicated_hyps.
apply between_only_one' in H37.
spliter.
apply between_comm in H6.
tauto.

apply H.
apply (colH_trans C C'); Col.
line_col C C' A.


induction H28.

line C B m (sym_not_equal H21).

assert(¬ ColH AB AC A).
intro.
apply H.
assert(Col A C AB).
apply(colH_trans A AC); Col.
apply(colH_trans A AB); Col.

assert(¬ Incid A m).
intro.
apply H.
line_col A B C.

assert(cut m AC AB).
unfold cut.
repeat split.
intro.
apply H.
apply(colH_trans C AC); Col.
line_col C AC B.

intro.
apply H.
line_col B C AB.
apply(colH_trans B AB); Col.

BC.

split.
col_line H14 m0.
lines_eq m m0.
assumption.
assumption.
apply cut_comm in H33.

assert(HH:= pasch AB AC A m H31 H32 H33).

induction HH.
unfold cut in H34.
spliter.
destruct H36 as [B' H36].
spliter.

assert(HH38:=H37).
apply between_col in HH38.
spliter.
assert(ColH A B B').
apply(colH_trans A AB); Col.
assert(B B').
intro.
subst B'.
unfold cut in H33.
spliter.
destruct H40 as [I H42].
spliter.
assert(I = BC).
apply(inter_uniquenessH C B AC AB); Col.
intro.
apply H.
apply (colH_trans C AC); Col.
line_col C B I.
apply between_col in H41.
spliter.
Col.
subst I.
apply between_only_one' in H37.
spliter.
apply between_comm in H11.
tauto.

apply H.
apply (colH_trans B B'); Col.
line_col B B' C.

unfold cut in H34.
spliter.
destruct H36 as [I H36].
spliter.

assert(HH38:= H37).
apply between_col in HH38.
spliter.
apply H.
assert(ColH C I A).
apply(colH_trans A AC); Col.
assert(ColH C I B).
line_col C I B.
apply (colH_trans C I); Col.
intro.
subst I.
apply between_only_one' in H37.
spliter.
apply between_comm in H9.
tauto.

line A B m H27.

assert(¬ ColH BC AC C).
intro.
apply H.
assert(Col B C AC).
apply(colH_trans C BC); Col.
apply(colH_trans C AC); Col.

assert(¬ Incid C m).
intro.
apply H.
line_col A B C.

assert(cut m BC AC).
unfold cut.
repeat split.
intro.
apply H.
apply(colH_trans B BC); Col.
line_col B BC A.

intro.
apply H.
line_col B A AC.
apply(colH_trans A AC); Col.

AB.

split.
col_line H12 m0.
lines_eq m m0.
assumption.
apply between_comm.
assumption.

assert(HH:= pasch BC AC C m H31 H32 H33).

induction HH.
unfold cut in H34.
spliter.
destruct H36 as [I H36].
spliter.

assert(HH38:= H37).
apply between_col in HH38.
spliter.
apply H.
assert(ColH B I C).
apply(colH_trans C BC); Col.
assert(ColH B I A).
line_col B I A.
apply (colH_trans B I); Col.
intro.
subst I.
apply between_only_one' in H37.
tauto.

unfold cut in H34.
spliter.
destruct H36 as [A' H36].
spliter.

assert(HH38:=H37).
apply between_col in HH38.
spliter.
assert(ColH C A A').
apply(colH_trans C AC); Col.
assert(A A').
intro.
subst A'.
unfold cut in H33.
spliter.
destruct H40 as [I H42].
spliter.
assert(I = AB).
apply(inter_uniquenessH B A BC AC); Col.
intro.
apply H.
apply (colH_trans B BC); Col.
line_col B A I.
apply between_col in H41.
spliter.
Col.
subst I.
clean_duplicated_hyps.
apply between_only_one' in H37.
spliter.
tauto.

apply H.
apply (colH_trans A A'); Col.
line_col A A' B.
Qed.

Lemma strong_pasch : (A B C : Point) (l : Line),
       ¬ ColH A B C ¬ Incid C l cut l A B cut l A C ¬cut l B C cut l B C ¬cut l A C.
Proof.
intros.
assert(HH:=pasch A B C l H H0 H1).
induction HH.
left.
split; auto.
apply(cut2_not_cut A B C l); auto.
right.
split; auto.
apply(cut2_not_cut B A C l); auto.
intro.
apply H; Col.
apply cut_comm.
assumption.
Qed.

Lemma out2_out : A B C D, C D BetH A B C BetH A B D BetH B C D BetH B D C.
Proof.
intros.
apply betH_expand in H0.
apply betH_expand in H1.
spliter.
assert(ColH B C D).
apply (colH_trans A B); Col.
apply between_one in H10; auto.
induction H10.
left; auto.
induction H10.
right.
Bet.
assert(ColH A C D).
apply (colH_trans A B); Col.
apply between_one in H11; auto.
induction H11.
assert(BetH B C D BetH A B D).
Bet.
spliter.
apply between_only_one' in H12.
spliter.
contradiction.
induction H11.
assert(BetH B D C BetH A B C).
Bet.
spliter.
apply between_only_one' in H12.
spliter.
apply between_comm in H10.
contradiction.
assert(BetH B A C BetH D B C).
Bet.
spliter.
apply between_only_one' in H12.
spliter.
contradiction.
Qed.

Lemma out2_out1 : A B C D, C D BetH A B C BetH A B D BetH A C D BetH A D C.
Proof.
intros.
apply betH_expand in H0.
apply betH_expand in H1.
spliter.
assert(ColH A C D).
apply(colH_trans A B); Col.
apply between_one in H10; auto.
induction H10.
intuition.
induction H10.
apply between_comm in H10.
intuition.

assert(BetH B A D BetH C B D).
apply(betH_trans0 C B A D); Bet.
spliter.
apply between_only_one' in H1.
spliter.
contradiction.
Qed.

Lemma betH2_out : A B C D, B C BetH A B D BetH A C D BetH A B C BetH A C B.
Proof.
intros.
apply betH_expand in H0.
apply betH_expand in H1.
spliter.
assert(ColH A B C).
apply (colH_trans A D); Col.
apply between_one in H10; auto.
induction H10.
left; auto.
induction H10.
right; Bet.

assert(BetH C A D BetH C B D).
apply(betH_trans C A B D); Bet.
induction H11.
apply between_only_one' in H11.
spliter.
contradiction.
Qed.

Hint Resolve betH2_out out2_out : bet.

Lemma segment_construction : A B C D,
     E, Bet A B E Cong B E C D.
Proof.
intros.
induction(eq_dec_pointsH C D).
subst D.
B.
split.
unfold Bet.
tauto.
unfold Cong.
right; tauto.

destruct (eq_dec_pointsH A B) as [HAB|HAB].
- subst.
  elim (other_point_exists B);intros A HBA.
  line B A l HBA.
   assert(HH:= cong_existence' C D l B H H0).
   ex_and HH F.
   ex_and H2 F'.
   apply betH_expand in H4.
   spliter.
    F.
   split.
   unfold Bet.
    auto.
   unfold Cong.
   repeat split;auto.
-
line A B l HAB.
assert(HH:= cong_existence' C D l B H H1).
ex_and HH F.
ex_and H2 F'.
apply betH_expand in H4.
spliter.
assert(ColH A F F').
line_col A F F'.

induction(eq_dec_pointsH A F).
subst F.
F'.
split.
left; auto.
left.
repeat split; auto.

induction (eq_dec_pointsH A F').
subst F'.
F.
split.
left; Bet.
left.
repeat split; auto.

apply between_one in H11; auto.
induction H11.
F'.
split.
assert(BetH B F A BetH F' B A).
Bet.
spliter.
left.
Bet.
left.
repeat split; auto.
induction H11.
F.
assert(BetH B F' A BetH F B A).
apply(betH_trans0 F B F' A); Bet.
spliter.
split.
left.
Bet.
left.
repeat split; auto.

induction(eq_dec_pointsH A B).
subst B.
F.
split.
right; Bet.
left.
repeat split; auto.

assert(BetH F' A B BetH F' B A).

apply(betH2_out F' A B F); Bet.
assert(BetH F A B BetH F B A).
apply(betH2_out F A B F'); Bet.
induction H15.
induction H16.

assert(BetH A F F' BetH A F' F).
apply(out2_out B A F F' H9); Bet.
induction H17;
apply between_only_one' in H17.
tauto.
spliter.
apply between_comm in H11.
tauto.
F.
split.
left.
Bet.
left.
repeat split; auto.
induction H16.
F'.
split.
left.
Bet.
left.
repeat split; auto.
assert(BetH B F F' BetH B F' F).
apply(out2_out A B F F' H9); Bet.
induction H17.
apply between_only_one' in H17.
tauto.
apply between_only_one' in H17.
spliter.
apply between_comm in H4.
tauto.
Qed.

Lemma lower_dim : A, B, C, ¬ (Bet A B C Bet B C A Bet C A B).
Proof.
assert(HH:=plan').
ex_and HH A.
ex_and H B.
ex_and H0 C.
A.
B.
C.
intro.
apply H.
induction H0;
unfold Bet in H0;
induction H0.
apply between_col in H0.
tauto.
induction H0; subst B;
apply False_ind;
apply H; Col.
induction H0.
apply between_col in H0; spliter; Col.
induction H0; subst C;
apply False_ind;
apply H; Col.
induction H0.
apply between_col in H0; spliter; Col.
induction H0; subst A;
apply False_ind;
apply H; Col.
Qed.

Lemma outH_dec : A B C, outH A B C ¬outH A B C.
Proof.
intros.
assert(HH:=colH_dec A B C).
induction HH.
induction(eq_dec_pointsH A B).
subst B.
right.
intro.
unfold outH in H0.
induction H0.
apply betH_distincts in H0.
tauto.
induction H0.
apply betH_distincts in H0.
tauto.
tauto.
induction(eq_dec_pointsH A C).
subst C.
right.
intro.
unfold outH in H1.
induction H1.
apply betH_distincts in H1.
tauto.
induction H1.
apply betH_distincts in H1.
tauto.
spliter.
subst B.
tauto.
induction(eq_dec_pointsH B C).
subst C.
left.
right; right.
split; auto.

apply between_one in H; auto.
induction H.
left.
left; auto.
induction H.
left.
right; left.
Bet.
right.
intro.
unfold outH in H3.
induction H3.
apply between_only_one' in H.
tauto.
induction H3.
apply between_only_one' in H.
tauto.
apply betH_distincts in H.
spliter.
contradiction.
right.
intro.
apply H.
unfold outH in H0.
induction H0.
apply between_col in H0.
tauto.
induction H0.
apply between_col in H0.
spliter.
Col.
spliter.
subst C.
Col.
Qed.

Lemma out_construction : A B X Y, X Y A B C, CongH A C X Y (outH A B C).
Proof.
intros.
line A B l H0.
assert(HH:=cong_existence' X Y l A H H1).
ex_and HH P.
ex_and H3 P'.
induction(outH_dec A B P).
P.
split; auto.
P'.
split; auto.
line_col A B P'.
apply betH_expand in H5.
spliter.
induction (eq_dec_pointsH B P').
subst P'.
right; right.
split; auto.
apply between_one in H9; auto.
induction H9.
left.
auto.
induction H9.
right; left.
Bet.
apply False_ind.
induction(eq_dec_pointsH B P).
subst P.
apply H8.
right; right; auto.
apply H8.
unfold outH.
assert(BetH A B P BetH A P B).
apply(out2_out P' A B P); Bet.
induction H16.
left; auto.
right; left; auto.
Qed.

Definition Para := fun l m¬ X, Incid X l Incid X m.

Definition ParaP A B C D := l m, Incid A l Incid B l Incid C m Incid D m Para l m.

Lemma segment_constructionH : A B C D : Point,
 A B C D E : Point, BetH A B E CongH B E C D.
Proof.
Proof.
intros.
assert(HH:= segment_construction A B C D).
ex_and HH E.
induction H1.
induction H2.
spliter.
E.
split; auto.
spliter.
subst E.
apply betH_distincts in H1.
tauto.
induction H1.
contradiction.
subst E.
induction H2.
tauto.
tauto.
Qed.
Definition is_line A B l := A B Incid A l Incid B l.

Lemma cut_exists : A l, ¬Incid A l B, cut l A B.
Proof.
intros.
assert(HH:= two_points_on_line l).
ex_and HH X.
ex_and p Y.

assert(A X).
intro.
subst X.
contradiction.
assert(HH:= between_out A X H3).
ex_and HH P.
P.
unfold cut.
repeat split; auto.
intro.
apply betH_expand in H4.
spliter.
assert(ColH X Y P).
line_col X Y P.
assert(ColH A X Y).
apply (colH_trans X P); Col.
unfold ColH in H11.
ex_and H11 m.
lines_eq l m.
contradiction.
X.
split; auto;
subst X.
Qed.

Lemma outH_col : A B C, outH A B C ColH A B C.
intros.
unfold outH in H.
induction H.
apply between_col in H.
auto.
induction H.
apply between_col in H.
Col.
spliter.
subst C.
Col.
Qed.

Lemma cut_distinct : A B l, cut l A B A B.
Proof.
intros.
unfold cut in H.
spliter.
ex_and H1 M.
apply betH_distincts in H2.
intuition.
Qed.

Lemma same_side_not_cut : A B l, same_side A B l ¬cut l A B.
Proof.
intros.
unfold same_side in H.
ex_and H P.

induction(colH_dec P A B).
intro.
unfold cut in ×.
spliter.
clean_duplicated_hyps.
ex_and H8 M.
ex_and H6 N.
assert(M N).
intro.
subst N.
assert(BetH M A B BetH M B A).
apply(out2_out P); Bet.
intro.
ex_and H4 Q.
apply betH_expand in H9.
intuition.
ex_and H4 R.
assert(ColH A B M).
induction H8;
apply between_col in H8;
Col.
apply betH_expand in H9; spliter.
assert(R= M).
line A B m H13.
col_line H1 mm.
lines_eq m mm.
col_line H14 nn.
lines_eq m nn.
col_line H10 pp.
lines_eq m pp.
assert(ColH A B R A B).
split; auto.
Col.
spliter.
apply(inter_incid_uniquenessH P R M l m H7 H17); Col.
subst R.
induction H8;
apply between_only_one' in H9;
spliter;
contradiction.
assert(A B).
ex_and H4 T.
apply betH_distincts in H9.
intuition.
col_line H1 m.
apply H8.
apply betH_expand in H3.
spliter.
col_line H16 mm.
lines_eq m mm.
apply betH_expand in H6.
spliter.
col_line H22 nn.
lines_eq m nn.
apply(inter_incid_uniquenessH P M N l m); auto.


apply cut_comm in H.
apply cut_comm in H0.
apply(cut2_not_cut P A B l); auto.
Qed.

Lemma cut_same_side_cut : P X Y l, cut l P X same_side X Y l cut l P Y.
Proof.
intros.
assert(HC := same_side_not_cut X Y l H0).
induction(eq_dec_pointsH X Y).
subst Y.
assumption.
assert(HH0:=H).
unfold cut in H.
spliter.
ex_and H3 A.

apply betH_expand in H4.
spliter.

induction(colH_dec P X Y).
unfold cut.

repeat split; auto.
intro.
assert(A Y).
intro.
subst Y.
unfold same_side in H0.
ex_and H0 M.
unfold cut in H11.
spliter.
contradiction.
apply betH_expand in H4.
spliter.
assert(ColH A X Y).
apply (colH_trans P X); Col.
col_line H16 m.
lines_eq l m.
contradiction.
A.
split; auto.

apply between_one in H9; auto.
induction H9.
assert(HH:= betH_trans0 P A X Y H4 H9).
intuition.
induction H9.

assert(A Y).
intro.
subst Y.
unfold same_side in H0.
ex_and H0 T.
unfold cut in H10.
spliter.
contradiction.
assert(BetH P A Y BetH P Y A).
apply(betH2_out P A Y X H10 H4); Bet.
induction H11.
auto.
exfalso.
apply HC.
unfold cut.
repeat split; auto.
unfold same_side in H0.
ex_and H0 T.
unfold cut in H12.
intuition.
A.
split; auto.
assert(HH:= betH_trans0 P Y A X H11 H4).
intuition.
exfalso.
apply HC.
unfold cut.
repeat split; auto.
intro.
unfold same_side in H0.
ex_and H0 T.
unfold cut in H11.
intuition.
A.
split; auto.
assert(BetH A P Y BetH X A Y).
apply(betH_trans0 X A P Y); Bet.
intuition.
intro.
subst Y.
apply cut_comm in HH0.
contradiction.


assert(¬Incid Y l).
intro.
unfold same_side in H0.
ex_and H0 T.
unfold cut in H11.
spliter.
contradiction.

assert(HP:=pasch P X Y l H9 H10 HH0).
induction HP.
assumption.
contradiction.
Qed.


Lemma isosceles_congaH : A B C, ¬ColH A B C CongH A B A C CongaH A B C A C B.
Proof.
intros.
apply (cong_5 A B C A C B).
assumption.
intro;apply H;Col.
assumption.
apply congH_sym;auto.
apply ncolH_distincts in H;spliter;auto.
apply conga_comm.
intro;apply H;Col.
Qed.

Lemma cong_distincts : A B C D, A B Cong A B C D C D.
Proof.
intros.
intro.
unfold Cong in H1.
spliter.
subst D.
induction H0;
tauto.
Qed.

Lemma cong_sym : A B C D, Cong A B C D Cong C D A B.
intros.
unfold Cong in ×.
induction H.
left; intuition.
apply congH_sym.
assumption.
assumption.
right.
tauto.
Qed.

Lemma cong_trans : A B C D E F, Cong A B C D Cong C D E F Cong A B E F.
Proof.
intros.
unfold Cong in ×.
induction H;
induction H0.
left.
intuition.
apply(cong_pseudo_transitivity C D A B E F).
apply congH_sym.
auto.
auto.
auto.
spliter.
subst D.
tauto.
spliter.
subst B.
contradiction.
right.
intuition.
Qed.

Lemma betH_not_congH : A B C, BetH A B C ¬ CongH A B A C.
Proof.
intros.
intro.
apply betH_expand in H.
spliter.
apply H2.
assert( P : Point, BetH B A P).
apply(between_out B A); auto.
ex_and H5 P.
apply between_comm in H6.
assert(HB:BetH P A C).
eapply (betH_trans2 _ _ B); auto.
apply construction_uniqueness with P A; auto.
Qed.

Lemma congH_permlr : A B C D, AB CD CongH A B C D CongH B A D C.
Proof.
intros.
apply cong_pseudo_transitivity with A B.
apply congH_perm.
auto.
apply cong_pseudo_transitivity with C D.
apply congH_sym.
assumption.
assumption.
apply congH_perm.
assumption.
Qed.

Lemma congH_perms : A B C D,
  AB CD
  CongH A B C D
 (CongH B A C D CongH A B D C CongH C D A B
  CongH D C A B CongH C D B A CongH D C B A CongH B A D C).
Proof.
intros.
repeat split;eauto using congH_permlr, congH_perm, cong_pseudo_transitivity.
Qed.

Lemma congH_perml : A B C D,
  A B C D CongH A B C D
  CongH B A C D.
Proof. intros A B C D HD1 HD2 HC; apply congH_perms in HC; spliter; auto. Qed.

Hint Resolve congH_sym congH_perm congH_perml cong_permr congH_refl
     cong_pseudo_transitivity congH_perms: cong.

Ltac Cong := eauto 3 with cong.

Lemma bet_cong3_bet : A B C A' B' C', A' B' B' C' A' C'
 BetH A B C Col A' B' C'
 CongH A B A' B' CongH B C B' C' CongH A C A' C'
 BetH A' B' C'.
Proof.
intros.
apply between_one in H3; auto.
induction H3.
assumption.
induction H3.
apply between_comm in H3.
apply betH_expand in H2.
spliter.

assert(HH:=segment_constructionH B C B C H8 H8).
ex_and HH B''.

apply betH_expand in H3.
apply betH_expand in H11.
spliter.
assert(BetH A B B'' BetH A C B'').
apply(betH_trans A B C B'' H2 H11 ).
spliter.

assert(CongH A B'' A' B').
   {
     apply(addition A C B'' A' C' B'); auto.
     apply(colH_trans B C); Col.
     apply bet_disjoint; auto.
     apply bet_disjoint; auto.
     apply(cong_pseudo_transitivity C B); Cong.
   }

assert(CongH A B'' A B).
   {
     apply betH_distincts in H21; spliter.
     apply (cong_pseudo_transitivity A' B'); Cong.
   }

assert(¬CongH A B A B'').
   {
      apply betH_not_congH; auto.
   }
exfalso.
apply H25.
apply betH_distincts in H21; spliter.
Cong.

apply between_comm in H3.
apply betH_expand in H2.
apply betH_expand in H3.
spliter.
clean_duplicated_hyps.
assert( E : Point, BetH C A E CongH A E A B).
   {
      apply(segment_constructionH C A A B); auto.
   }
ex_and H8 B''.
apply betH_expand in H8.
spliter.
assert(CongH C B'' C' B').
   {
     apply(addition C A B'' C' A' B'); auto.
     apply bet_disjoint; auto.
     apply bet_disjoint; auto.
     Cong.
     Cong.
   }

assert(BetH B A B'' BetH C B B'').
   {
      apply(betH_trans0 C B A B'');
      Bet.
   }
spliter.

assert(¬CongH C B C B'').
   {
      apply betH_not_congH.
      assert(HH:=(betH_trans0 C B A B''));auto.
   }
exfalso.
apply H23.
apply betH_distincts in H3; spliter.
apply (cong_pseudo_transitivity C' B'); eauto with cong.
Qed.

Lemma betH_congH3_outH_betH : A B C A' B' C',
  BetH A B C outH A' B' C' CongH A C A' C' CongH A B A' B' BetH A' B' C'.
Proof.
intros.
apply betH_expand in H.
spliter.
unfold outH in ×.
induction H0.
assumption.
induction H0.
assert(HH:=segment_constructionH A' B' B C).
ex_and HH C''.
apply betH_expand in H7.
spliter.
exfalso.
assert(CongH A' C'' A C).
eapply(addition A' B' C'' A B C); auto.
apply bet_disjoint; auto.
apply bet_disjoint; auto.
Cong.
assert(BetH C' B' C'' BetH A' C' C'').
   {
      apply(betH_trans0 A' C' B' C''); auto.
   }
spliter.
assert(HH:= betH_not_congH A' C' C'' H15).
apply HH.
apply(cong_pseudo_transitivity A C); Cong.
apply betH_expand in H0.
tauto.
apply betH_expand in H0.
tauto.
spliter.
subst C'.
assert(HH:=betH_not_congH A B C H).
exfalso.
apply HH.
apply (cong_pseudo_transitivity A' B'); Cong.
Qed.

Lemma outH_sym : A B C,
  A C outH A B C outH A C B.
Proof.
intros.
unfold outH in ×.
decompose [or] H0;clear H0.
auto.
auto.
spliter;subst;auto.
Qed.

Lemma soustraction_betH :
A B C A' B' C' : Point,
      BetH A B C
      BetH A' B' C'
      CongH A B A' B' CongH A C A' C' CongH B C B' C'.
Proof.
intros.
apply betH_expand in H.
apply betH_expand in H0.
spliter.
elim (segment_constructionH A' B' B C H3 H8).
intros C1 [HC1 HC2].
assert (CongH A C A' C1).
assert(HD := betH_distincts _ _ _ HC1); spliter.
apply addition_betH with B B';auto using congH_sym.
elim (between_out B A).
intros X HX.
elim (between_out B' A').
intros X' HX'.
assert (BetH X A C).
 apply (betH_trans2 X A B C);auto using between_comm.
assert (BetH X' A' C1).
 apply (betH_trans2 X' A' B' C1);auto using between_comm.
assert (C'=C1).
 {
 apply construction_uniqueness with X' A'; auto.
 apply (betH_trans2 X' A' B' C'); auto using between_comm.
 apply cong_pseudo_transitivity with A C; auto using congH_sym.
 }
subst.
auto using congH_sym.
auto.
auto.
Qed.

Lemma ncolH_expand : A B C, ¬ ColH A B C ¬ ColH A B C A B B C A C.
Proof.
intros.
split; auto.
split.
intro.
subst B.
apply H.
Col.
split; intro;
subst C; apply H; Col.
Qed.

Lemma betH_outH__outH : A B C D,
  BetH A B C outH B C D outH A C D.
Proof.
intros.
destruct H0.
unfold outH.
left.
apply (betH_trans A B C D);auto.
destruct H0.
unfold outH.
right;left.
apply between_comm;
apply (betH_trans0 C D B A);auto using between_comm.
spliter. subst.
apply outH_trivial.
apply betH_expand in H;spliter;auto.
Qed.

First case of congruence of triangles

Lemma th12: A B C A' B' C',
  ¬ ColH A B C
  ¬ ColH A' B' C'
  CongH A B A' B'
  CongH A C A' C'
  CongaH B A C B' A' C'
  CongaH A B C A' B' C' CongaH A C B A' C' B' CongH B C B' C'.
Proof.
intros.
repeat split.
apply cong_5;auto.
apply cong_5;auto.
intro;apply H;Col.
intro;apply H0;Col.
apply congaH_permlr;auto.
assert (T:=ncolH_distincts A B C H).
assert (U:=ncolH_distincts A' B' C' H0).
spliter.
elim (out_construction B' C' B C H8 H5).
intros D' [HD1 HD2].
destruct (eq_dec_pointsH B' D').
 {
 subst.
 unfold outH in HD2.
 destruct HD2.
 apply betH_expand in H10;intuition.
 destruct H10.
 apply betH_expand in H10;intuition.
 intuition.
 }
assert (CongaH A B C A' B' C') by ( apply cong_5;auto).

assert (CongaH B A C B' A' D').
 apply (cong_5 B A C B' A' D').
 intro;apply H;Col.
 intro;apply H0.
  apply outH_col in HD2.
  apply colH_trans with B' D';Col.
 apply congH_permlr;auto.
 apply congH_sym;auto.
 apply congaH_outH_congaH with A C A' C'; auto using outH_trivial.

assert (outH A' C' D').
 apply (hcong_4_uniqueness B A C A' C' B' C' D');try assumption.
intro;apply H0;Col.
intro;apply H;Col.

apply same_side_prime_refl;auto.
unfold same_side'.
split.
auto.
intros.
unfold same_side.
destruct (between_out D' B').
 auto.
x.
unfold cut.
repeat split.
intro.
apply H0; l;auto.
intro.
apply outH_col in HD2.
destruct HD2.
spliter.
apply betH_expand in H15.
spliter.
destruct H23.
spliter.
assert (EqL x1 l).
apply line_uniqueness with B' x;auto.
rewrite H26 in ×.
assert (EqL x0 l).
apply line_uniqueness with B' D';auto.
rewrite H27 in ×.
apply H0.
l;auto.
B'.
split.
auto.
unfold outH in HD2.
destruct HD2.
apply (betH_trans0 D' C' B' x);auto using between_comm.
destruct H16.
apply between_comm;apply (betH_trans2 x B' D' C');auto using between_comm.
spliter;subst;auto.
intro.
apply outH_col in HD2.
assert (ColH A' B' D').
l;auto.
apply H0.
apply (colH_trans B' D' A' B' C');Col.
intro.
apply outH_col in HD2.
destruct HD2.
spliter.
apply betH_expand in H15.
spliter.
destruct H23.
spliter.
assert (EqL x1 l).
apply line_uniqueness with B' x;auto.
rewrite H26 in ×.
assert (EqL x0 l).
apply line_uniqueness with B' D';auto.
rewrite H27 in ×.
apply H0.
l;auto.

B'.
split.
auto.
auto.

assert (C'=D').

line B' C' lB'C' H5.
line A' C' lA'C' H6.
apply inter_incid_uniquenessH with A' lB'C' lA'C';auto.
intro.
apply H0.
lB'C';auto.
apply outH_col in HD2.
destruct HD2.
spliter.
assert (EqL x lB'C').
apply line_uniqueness with B' C';auto.
rewrite H21 in H20.
auto.
apply outH_col in H13.
destruct H13.
spliter.
assert (EqL x lA'C').
apply line_uniqueness with A' C';auto.
rewrite H20 in H19.
auto.
subst.
auto using congH_sym.
Qed.

Lemma th14: A B C D A' B' C' D',
  ¬ ColH A B C
  ¬ ColH A' B' C'
  CongaH A B C A' B' C'
  BetH A B D
  BetH A' B' D'
  CongaH C B D C' B' D'.
Proof.
intros.
apply betH_expand in H2.
apply betH_expand in H3.
spliter.
assert (T:=ncolH_distincts A B C H).
assert (U:=ncolH_distincts A' B' C' H0).
spliter.
elim (out_construction B' A' A B);try solve [auto].
intros A'' [HA1 HA2].
elim (out_construction B' C' B C);try solve [auto].
intros C'' [HC1 HC2].
elim (out_construction B' D' B D);try solve [auto].
intros D'' [HD1 HD2].
assert (CongaH B A C B' A'' C''
       CongaH B C A B' C'' A'' CongH A C A'' C'').
 {
  apply (th12 B A C B' A'' C'').
  intro;apply H;Col.
  intro;apply H0.
  {

  destruct HA2.
   apply betH_expand in H19.
   spliter.
  destruct HC2.
   apply betH_expand in H24.
   spliter.
   apply colH_trans with B' A'';Col.
   apply colH_trans with B' C'';Col.
   destruct H24.
   apply betH_expand in H24.
   spliter.
   apply colH_trans with B' A'';Col.
   apply colH_trans with B' C'';Col.
   spliter;subst.
   exfalso. apply H0.
   apply colH_trans with B' A'';Col.
  destruct H19.
  apply betH_expand in H19.
  spliter.
  destruct HC2.
     apply betH_expand in H24.
   spliter.
   apply colH_trans with B' A'';Col.
   apply colH_trans with B' C'';Col.
   destruct H24.
   apply betH_expand in H24.
   spliter.
   apply colH_trans with B' A'';Col.
   apply colH_trans with B' C'';Col.
   spliter;subst.
   exfalso. apply H0.
   apply colH_trans with B' A'';Col.
   spliter;subst.
   exfalso. apply H0.
   destruct HC2.
   apply betH_expand in H20;spliter.
   apply colH_trans with B' C'';Col.
   destruct H20.
   apply betH_expand in H20;spliter.
   apply colH_trans with B' C'';Col.
   spliter;subst.
   apply colH_trans with A'' B';Col.
  }
  apply outH_expand in HA2; spliter.
  apply congH_sym; auto.
  apply cong_pseudo_transitivity with A B.
  auto using congH_sym.
  apply congH_perm; auto.
  apply outH_expand in HC2; spliter.
  auto using congH_sym.
  apply congaH_outH_congaH with A C A' C'; auto using outH_trivial.
 }
spliter.
assert (BetH A'' B' D'')
  by (apply betH_outH2__betH with A' D';auto).
apply betH_expand in H21.
spliter.
assert (CongH A D A'' D'').
 {
   apply addition_betH with B B';auto.
   apply congH_perms in HA1;intuition.
   apply congH_perms in HD1;intuition.
 }
assert (¬ ColH A C D).
 intro; apply H; apply colH_trans with A D;Col.
assert (¬ ColH A'' C'' D'').
 intro; apply H0.
   apply outH_expand in HA2.
   apply outH_expand in HC2.
   apply outH_expand in HD2.
   spliter;ColHR.
assert (T:=ncolH_distincts A C D H27).
assert (U:=ncolH_distincts A'' C'' D'' H28).
spliter.
assert (CongaH A C D A'' C'' D''
       CongaH A D C A'' D'' C'' CongH C D C'' D'').
 {
  apply (th12 A C D A'' C'' D'');try assumption.
  apply congaH_outH_congaH with C B C'' B'; auto using congaH_permlr, outH_trivial.
  unfold outH;left;auto.
  left.
  apply betH_outH2__betH with A' D';auto.
 }
spliter.

assert (¬ ColH D B C) by (intro; apply H; ColHR).
assert (¬ ColH D'' B' C'').
  apply outH_expand in HA2.
   apply outH_expand in HC2.
   apply outH_expand in HD2.
  intro;apply H0;spliter;ColHR.
assert (T:=ncolH_distincts D B C H38).
assert (U:=ncolH_distincts D'' B' C'' H39).
spliter.
assert (CongaH D B C D'' B' C'').
  {
   apply (cong_5 D B C D'' B' C'').
   assumption.
   assumption.
   apply congH_perms in HD1;spliter;auto.
   apply congH_perms in H37;spliter;auto.
   apply congaH_outH_congaH with A C A'' C'';auto using outH_trivial.
   unfold outH.
   right;left;auto using between_comm.
   right;left.
   apply betH_outH2__betH with D' A';auto using between_comm.
  }
apply congaH_permlr.
apply congaH_outH_congaH with D C D'' C'';auto using outH_trivial, outH_sym.
Qed.

Lemma congH_colH_betH: A B I,
 AB AI BI
 CongH I A I B
 ColH I A B
 BetH A I B.
Proof.
intros.
apply between_one in H3;auto.
decompose [or] H3;clear H3.
- exfalso.
  apply (betH_not_congH I A B);auto.
- exfalso.

  assert (T:=betH_not_congH I B A).
  apply T; auto using between_comm, congH_sym.
- assumption.
Qed.

Definition cut' A B X Y := X Y l, Incid X l Incid Y l cut l A B.

Global Instance cut_morphism : Proper(EqL ==> eq ==> eq ==> iff) cut.
Proof.
intro.
intros.
intro.
intros.
intro.
intros.
subst.
unfold cut.
rewrite H .
intuition.

elim H3;intros I;intros;spliter; I;split;try rewrite <- H;auto.
elim H3;intros I;intros;spliter; I;split;try rewrite H;auto.
Qed.

Global Instance same_side_morphism : Proper(eq ==> eq ==> EqL ==> iff) same_side.
Proof.
unfold Proper.
intro.
intros.
intro.
intros.
intro.
intros.
unfold same_side.
subst.
split;intro.
destruct H.
x;spliter;split;auto.
rewrite H1 in *;auto.
rewrite H1 in *;auto.
destruct H.
x;spliter;split;auto.
rewrite H1 in *;auto.
rewrite H1 in *;auto.
Qed.

Lemma plane_separation : A B X Y,
  ¬ ColH A X Y ¬ ColH B X Y
  cut' A B X Y same_side' A B X Y.
Proof.
intros A B X Y HNC1 HNC2; assert (HD1 : X Y) by (intro; subst; Col).
line X Y l HD1; destruct (cut_exists A l) as [C HC1];
[intro; apply HNC1; l; auto|].
elim (eq_dec_pointsH A B); [intro; subst; right; apply same_side_prime_refl;
                            intro; apply HNC1; Col|intro HD2].
assert (HD3 : A C) by (apply cut_distinct with l; auto).
elim (eq_dec_pointsH B C).

  {
  intro; subst; left; split; auto; intro m; intros.
  destruct HC1 as [HNI1 [HNI2 [I [HI HBet]]]].
  split; [apply (line_uniqueness _ Y m l) in H; try rewrite H; auto|].
  split; [apply (line_uniqueness _ Y m l) in H; try rewrite H; auto|].
   I; split; auto; apply (line_uniqueness _ Y m l) in H;
  auto; rewrite H; auto.
  }

  {
  intro HD4; elim (colH_dec A C B).

    {
    intro HCol1; assert (HI := HC1); destruct HI as [_ [_ [I [HInc HCol2]]]].
    apply between_col in HCol2; assert (HE : ColH A I B) by ColHR.
    apply between_one in HE; auto;
    [|intro; subst; apply HNC1|intro; subst; apply HNC2]; try l; auto.
    assert (HNI : ¬ Incid A l) by (intro; apply HNC1; l; auto).
    elim HE; clear HE; intro HE; try (elim HE; clear HE; intro HE);
    [left|right|right]; try (split; auto; intro m; intros;
                             apply (line_uniqueness _ Y m l) in H;
                             try rewrite H in *; auto;
                             apply out_same_side with I; unfold outH; auto).
    split; [intro; subst; Col|intro m; intros].
    split; [intro; apply HNC1; m; auto|].
    split; [intro; apply HNC2; m; auto|].
     I; split; auto.
    apply (line_uniqueness _ Y m l) in H; try rewrite H; auto.
    }

    {
    intro HNC3; elim (pasch A C B l); auto; intro HC2;
    try (apply HNC2; l; auto); [left|right];
    split; auto; intro m; intros;
    apply (line_uniqueness _ Y m l) in H; try rewrite H;
    try ( C; split); auto; apply cut_comm; auto.
    }
  }
Qed.

Lemma same_side_comm : A B l,
  same_side A B l same_side B A l.
Proof.
intros.
unfold same_side in ×.
elim H;intros.
x;spliter;split;auto using cut_comm.
Qed.

Lemma same_side_not_incid : A B l,
  same_side A B l ¬ Incid A l ¬ Incid B l.
Proof.
intros.
unfold same_side in ×.
destruct H as [P [HP1 HP2]].
unfold cut in ×.
spliter;auto.
Qed.

Lemma out_same_side' : X Y A B C l , X Y
  Incid X l Incid Y l Incid A l ¬ Incid B l outH A B C
  same_side' B C X Y.
Proof.
intros.
assert(HH:= out_same_side A B C l H2 H3 H4).
unfold same_side'.
split; auto.
intros.
lines_eq l l0.
assumption.
Qed.

Lemma same_side_trans : A B C l,
  same_side A B l same_side B C l same_side A C l.
Proof.
intros.
unfold same_side in H.
destruct H as [X [HX1 HX2]].
assert (cut l X C)
 by (apply (cut_same_side_cut X B C l);auto using cut_comm).
unfold same_side.
X.
split;auto using cut_comm.
Qed.

Lemma Incid_not_Incid__not_colH : A B C l,
 AB
 Incid A l
 Incid B l
 ¬ Incid C l
 ¬ ColH A B C.
Proof.
intros.
intro.
elim H3.
intros.
spliter.
assert (EqL l x) by (eauto using line_uniqueness).
rewrite H7 in ×.
intuition.
Qed.

Lemma same_side_prime_not_colH : A B C D,
 same_side' A B C D ¬ ColH A C D ¬ ColH B C D.
Proof.
intros.
unfold same_side' in ×.
spliter.
elim (line_existence C D H).
intros l [HL1 HL2].
assert (same_side A B l) by auto.
apply same_side_not_incid in H1.
spliter.
split.
assert (¬ ColH C D A).
apply Incid_not_Incid__not_colH with l;auto.
intuition Col.
assert (¬ ColH C D B).
apply Incid_not_Incid__not_colH with l;auto.
intuition Col.
Qed.

Lemma OS2__TS : O X Y Z,
  same_side' Y Z O X same_side' X Y O Z cut' X Z O Y.
Proof.
intros O X Y Z HOS1 HOS2.
destruct (between_out Z O) as [Z' HZ']; [unfold same_side' in *; spliter; auto|].
assert (HTS : cut' Y Z' O X).
  {
  assert (HD1 : O X) by (unfold same_side' in *; spliter; auto).
  assert (HD2 : O Z) by (unfold same_side' in *; spliter; auto).
  split; [auto|intro l; intros].
  apply cut_comm; apply cut_same_side_cut with Z;
  [|destruct HOS1 as [_ HOS1]; apply same_side_comm; apply HOS1; auto].
  destruct (same_side_not_incid Y Z l) as [HNI1 HNI2];
  [destruct HOS1 as [_ HOS1]; apply HOS1; auto|].
  assert (HNC := Incid_not_Incid__not_colH O X Z l HD1).
  split; [|split; auto; O; split; try apply between_comm; auto].
  intro; apply HNC; auto.
  assert (HC1 : ColH O X Z') by ( l; auto).
  assert (HD3 := betH_distincts _ _ _ HZ'); spliter.
  assert (HC2 := between_col _ _ _ HZ'); ColHR.
  }
split; [destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [HNC _];
        intro; subst; apply HNC; Col|intro l; intros].
apply cut_comm; apply cut_same_side_cut with Z'.

  {
  assert (HD1 : O X) by (unfold same_side' in *; spliter; auto).
  assert (HD2 : O Z) by (unfold same_side' in *; spliter; auto).
  destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC].
  split; [intro; apply HNC; l; auto|].
  assert (HD3 : O Y) by (intro; subst; apply HNC; Col).
  split; [intro| O; auto].
  assert (HD4 := betH_distincts _ _ _ HZ'); spliter.
  assert (HC1 : ColH O Y Z') by ( l; auto).
  assert (HC2 := between_col _ _ _ HZ').
  apply HNC; apply between_col in HZ'; ColHR.
  }

  {
  destruct HTS as [HD1 HTS]; line O X m HD1.
  assert (HCut : cut m Y Z') by (apply HTS; auto).
  assert (HX' := HCut); destruct HX' as [HNI1 [HNI2 [X' [HI HBet]]]].
  apply same_side_trans with X'.

    {
    apply out_same_side with Y; try (right; left); auto.
    destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC].
    intro; assert (HC1 : ColH O Y Z') by ( l; auto).
    assert (HD3 := betH_distincts _ _ _ HZ'); spliter.
    assert (HC2 := between_col _ _ _ HZ').
    apply HNC; apply between_col in HZ'; ColHR.
    }

    {
    assert (HC : ColH O X X') by ( m; auto).
    destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [HNC1 _].
    apply same_side_comm; apply out_same_side with O; auto;
    [intro; apply HNC1; l; auto|].
    elim (eq_dec_pointsH X X'); intro HD2; [subst; apply outH_trivial; auto|].
    destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [_ HNC2].
    assert (HD3 := betH_distincts _ _ _ HZ'); spliter.
    assert (HC2 := between_col _ _ _ HZ').
    assert (HC3 := between_col _ _ _ HBet).
    elim (eq_dec_pointsH O X'); intro HD3; [subst; exfalso; apply HNC2; ColHR|].
    assert (HC4 := HC); apply between_one in HC; auto.
    elim HC; clear HC; intro HC; [left; auto|].
    elim HC; clear HC; intro HFalse; [right; left; apply between_comm; auto|].
    assert (HD4 : O Z) by auto; line O Z o HD4.
    assert (HOS3 : same_side X Y o)
      by (destruct HOS2 as [_ HOS]; apply HOS; auto).
    exfalso; apply (same_side_not_cut _ _ _ HOS3).
    apply cut_same_side_cut with X'.

      {
      destruct (same_side_prime_not_colH _ _ _ _ HOS1) as [_ HNC3].
      split; [intro; apply HNC3; o; auto|].
      split;[| O; auto].
      intro; assert (ColH X' O Z) by ( o; auto); apply HNC3; ColHR.
      }

      {
      apply out_same_side with Z'; try (left; apply between_comm; auto).

        {
        destruct HC2 as [p [HI' ]]; spliter.
        apply (line_uniqueness _ O o) in HI'; auto; rewrite HI'; auto.
        }

        {
        intro; assert (ColH O X' Z) by ( o; auto).
        destruct (same_side_prime_not_colH _ _ _ _ HOS2) as [HNC3 _].
        apply HNC3; ColHR.
        }
      }
    }
  }
Qed.

Lemma th15: H K O L H' K' O' L',
  ¬ ColH H O L ¬ ColH H' O' L' ¬ ColH K O L ¬ ColH K' O' L'
  ¬ ColH H O K ¬ ColH H' O' K'
  (cut' H K O L cut' H' K' O' L') (same_side' H K O L same_side' H' K' O' L')
  CongaH H O L H' O' L' CongaH K O L K' O' L'
  CongaH H O K H' O' K'.
Proof.
assert (th15_aux : H K O L H' K' O' L',
                     ¬ ColH H O L ¬ ColH H' O' L'
                     ¬ ColH K O L ¬ ColH K' O' L'
                     ¬ ColH H O K ¬ ColH H' O' K'
                     same_side' H K O L same_side' H' K' O' L'
                     CongaH H O L H' O' L' CongaH K O L K' O' L'
                     CongaH H O K H' O' K').
  {
  assert (th15_aux : H K O L H' K' O' L',
                       ¬ ColH H O L ¬ ColH H' O' L'
                       ¬ ColH K O L ¬ ColH K' O' L'
                       ¬ ColH H O K ¬ ColH H' O' K'
                       same_side' H K O L same_side' H' K' O' L'
                       cut' K L O H
                       CongaH H O L H' O' L' CongaH K O L K' O' L'
                       CongaH H O K H' O' K').
    {
    intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6.
    intros HOS1 HOS2 HCut' HConga1 HConga2.
    destruct (out_construction O' K' O K) as [K'' [HCong1 Hout1]];
    try (intro; subst; Col).
    destruct (out_construction O' L' O L) as [L'' [HCong2 Hout2]];
    try (intro; subst; Col).
    apply (congaH_outH_congaH _ _ _ _ _ _ K L K'' L'') in HConga2; auto;
    try apply outH_sym; try apply outH_trivial; auto; try (intro; subst; Col).
    assert (HD1 : O H) by (intro; subst; Col).
    line O H l HD1; assert (HCut : cut l K L)
      by (destruct HCut' as [_ HCut]; apply HCut; auto).
    destruct HCut as [HNI1 [HNI2 [I [HI HBet1]]]].
    assert (HD2 : O I)
      by (intro; subst; apply HNC3; apply between_col; auto).
    assert (HI' : I',
                    O' I' I' L''
                    outH O H I outH O' H' I'
                    ColH O' I' H' CongH O' I' O I
                    CongaH I O L I' O' L'').
      {
      assert (outH O I H).
        {
        assert (HE : ColH O I H) by ( l; auto).
        elim (eq_dec_pointsH H I); intro HD3;
        [subst; apply outH_trivial; auto|].
        apply between_one in HE; auto;
        elim HE; clear HE; intro HE; [left; auto|].
        elim HE; clear HE; intro HFalse;
        [right; left; apply between_comm; auto|].
        assert (HD4 : O L) by (intro; subst; Col).
        line O L m HD4; destruct HOS1 as [_ HOS1].
        assert (HF : same_side H K m) by (apply HOS1; auto).
        exfalso; apply (same_side_not_cut _ _ _ HF).
        apply cut_same_side_cut with I.

          {
          split; [intro; apply HNC1; m; auto|].
          split; [| O; split; try apply between_comm; auto].
          intro; assert (ColH O L I) by ( m; auto).
          apply between_col in HFalse; apply HNC1; ColHR.
          }

          {
          apply out_same_side with L; try (left; apply between_comm); auto.
          intro; assert (ColH O L I) by ( m; auto).
          apply between_col in HFalse; apply HNC1; ColHR.
          }
        }
      destruct (out_construction O' H' O I) as [I' [HCong3 Hout4]];
      try (intro; subst; Col).
      apply (congaH_outH_congaH _ _ _ _ _ _ I L I' L'') in HConga1; auto;
      try apply outH_sym; try apply outH_trivial;
        auto; try (intro; subst; Col).
      assert (O' I') by (apply outH_expand in Hout4; spliter; auto).
      assert (I' L'').
        {
        intro; subst; apply same_side_prime_not_colH in HOS2;
        destruct HOS2 as [HNC _]; apply HNC.
        apply outH_expand in Hout2;
        apply outH_expand in Hout4; spliter; ColHR.
        }
       I'; split; auto; split; auto; split; [apply outH_sym; auto|].
      split; auto; split; try apply outH_col; try apply outH_sym; auto.
      }
    assert (HCol1 : ColH O I H) by ( l; auto); clear HConga1.
    destruct HI' as [I' [HD3 [HD4 [Hout3 [Hout4 [HCol2 [HCong3 HConga1]]]]]]].
    assert (HT : CongaH O I L O' I' L'' CongaH O L I O' L'' I'
                 CongH I L I' L'').
      {
      assert (O L) by (intro; subst; Col).
      assert (O' L'') by (apply outH_expand in Hout2; spliter; auto).
      apply outH_expand in Hout2; spliter.
      apply th12; Cong; try intro; [apply HNC1|apply HNC2]; ColHR.
      }
    destruct HT as [_ [HConga3 HCong4]].
    assert (HT : CongaH O K L O' K'' L'' CongaH O L K O' L'' K''
                 CongH K L K'' L'').
      {
      assert (O K) by (intro; subst; Col).
      assert (O L) by (intro; subst; Col).
      apply outH_expand in Hout1; apply outH_expand in Hout2; spliter.
      apply th12; Cong; intro; [apply HNC3|apply HNC4]; Col; ColHR.
      }
    destruct HT as [HConga4 [HConga5 HCong5]].
    assert (HBet2 : BetH K'' I' L'').
      {
      assert (Hout5 : outH L'' I' K'').
        {
        assert (O K) by (intro; subst; Col).
        assert (O L) by (intro; subst; Col).
        apply outH_expand in Hout1; apply outH_expand in Hout2; spliter.
        apply hcong_4_uniqueness with O L K H' O'; auto;
        [intro; apply HNC2; ColHR|intro; apply HNC3; Col| | |].

          {
          apply congaH_outH_congaH with O I O' I'; try apply outH_trivial; auto.
          left; apply between_comm; auto.
          }

          {
          assert (HD5 : O' L'') by auto; line O' L'' m HD5.
          apply out_same_side' with O' m; auto; intro; apply HNC2.
          assert (ColH O' L'' H') by ( m; auto); ColHR.
          }

          {
          split; auto; destruct HOS2 as [_ HOS2]; intro m; intros.
          assert (HCol3 : ColH O' L' L'') by auto.
          destruct HCol3 as [o [HI1 [HI2 HI3]]]; assert (HEq := HI1).
          apply (line_uniqueness _ L'' m _) in HEq; auto; rewrite HEq.
          apply same_side_trans with K'; try apply HOS2; auto.
          apply out_same_side with O'; auto; intro; apply HNC4; o; auto.
          }
        }
      apply between_comm; assert (K L) by (intro; subst; Col).
      apply outH_expand in Hout5; apply betH_expand in HBet1; spliter.
      apply betH_congH3_outH_betH with L I K; try apply between_comm; Cong.
      }
    assert (HT : CongaH K O I K'' O' I' CongaH K I O K'' I' O'
                 CongH O I O' I').
      {
      assert (K O) by (intro; subst; Col).
      apply outH_expand in Hout1; apply outH_expand in Hout2;
      apply betH_expand in HBet1; apply betH_expand in HBet2; spliter.
      assert (CongH I' K'' I K)
        by (apply soustraction_betH with L'' L;
            try apply between_comm; auto with cong).
      apply th12; auto with cong; try apply congaH_outH_congaH with O L O' L'';
      try (intro; apply HNC3; ColHR); try (intro; apply HNC4; ColHR);
      try apply outH_trivial; try (right; left); auto.
      }
    destruct HT as [HConga6 _]; apply congaH_permlr.
    apply outH_expand in Hout1; apply outH_expand in Hout3;
    apply outH_expand in Hout4; spliter.
    apply congaH_outH_congaH with K I K'' I'; try apply outH_trivial;
    try apply outH_sym; auto; intro; subst; Col.
    }
  intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6.
  intros HOS1 HOS2 HConga1 HConga2; elim (plane_separation K L O H); intro HS;
  [apply th15_aux with L L'; auto| |apply HNC5; Col|apply HNC1; Col].
  apply congaH_permlr; apply th15_aux with L L'; try solve[intro; Col]; auto;
  [| |apply OS2__TS; auto]; split; try (intro l ; subst; Col); intros;
  apply same_side_comm; [destruct HOS1 as [_ HOS1]; apply HOS1; auto|].
  destruct HOS2 as [_ HOS2]; apply HOS2; auto.
  }
intros H K O L H' K' O' L' HNC1 HNC2 HNC3 HNC4 HNC5 HNC6 HE HConga1 HConga2.
elim HE; clear HE; intros [HTS1 HTS2]; [|apply th15_aux with L L'; auto].
destruct (between_out H O) as [SH HSH]; [intro; subst; Col|].
destruct (between_out H' O') as [SH' HSH']; [intro; subst; Col|].
assert (HConga3 : CongaH SH O L SH' O' L')
  by (apply congaH_permlr; apply th14 with H H'; auto).
assert (HConga4 : CongaH SH O K SH' O' K').
  {
  assert (HD1 := betH_distincts _ _ _ HSH); spliter.
  assert (HD2 := betH_distincts _ _ _ HSH'); spliter.
  assert (HC1 := between_col _ _ _ HSH).
  assert (HC2 := between_col _ _ _ HSH').
  apply th15_aux with L L'; auto;
  try (intro; apply HNC1; ColHR); try (intro; apply HNC2; ColHR);
  try (intro; apply HNC5; ColHR); try (intro; apply HNC6; ColHR).

    {
    split; [intro; subst; Col|intro l; intros; H; split];
    [|destruct HTS1 as [_ HTS1]; apply cut_comm; apply HTS1; auto].
    split; [intro; apply HNC1; assert (ColH O L SH) by ( l; auto); ColHR|].
    split; [intro; apply HNC1; l; auto|
             O; split; try apply between_comm; auto].
    }

    {
    split; [intro; subst; Col|intro l; intros; H'; split];
    [|destruct HTS2 as [_ HTS2]; apply cut_comm; apply HTS2; auto].
    split; [intro; apply HNC2; assert (ColH O' L' SH') by ( l; auto); ColHR|].
    split; [intro; apply HNC2; l; auto|
             O'; split; try apply between_comm; auto].
    }
  }
assert (HD1 := betH_distincts _ _ _ HSH); spliter.
assert (HD2 := betH_distincts _ _ _ HSH'); spliter.
assert (HC1 := between_col _ _ _ HSH).
assert (HC2 := between_col _ _ _ HSH').
apply congaH_permlr; apply th14 with SH SH'; try apply between_comm; auto;
intro; try (apply HNC5; ColHR); try (apply HNC6; ColHR).
Qed.

Lemma th17:
  X Y Z1 Z2 I,
 ¬ ColH X Y Z1
 ¬ ColH X Y Z2
 ColH X I Y
 BetH Z1 I Z2
 CongH X Z1 X Z2
 CongH Y Z1 Y Z2
 CongaH X Y Z1 X Y Z2.
Proof.
intros.
induction (colH_dec Y Z1 Z2).
 induction (colH_dec X Z1 Z2).
 {
  apply betH_expand in H2.
  spliter.
  exfalso.
  apply H0;ColHR.
 }
 {
 assert (CongaH X Z1 Z2 X Z2 Z1)
  by (apply (isosceles_congaH X Z1 Z2);auto).

 apply congaH_permlr.
 apply (cong_5 Z1 Y X Z2 Y X).
  intro;apply H;Col.
  intro;apply H0;Col.
  apply congH_perms in H4;spliter; auto; try (intro; subst; Col).
  apply congH_perms in H3;spliter; auto; try (intro; subst; Col).
  apply congaH_permlr.
  assert (BetH Z1 Y Z2).
    {
     apply ncolH_distincts in H;
     apply ncolH_distincts in H0;
     apply congH_colH_betH;apply betH_expand in H2;spliter;auto.
    }
  apply congaH_outH_congaH with X Z2 X Z1;auto using outH_trivial.
  apply ncolH_distincts in H;spliter;auto using outH_trivial.
  unfold outH. right;left;auto.
   apply ncolH_distincts in H0;spliter;auto using outH_trivial.
  unfold outH. right;left;auto using between_comm.
  }
  induction (colH_dec X Z1 Z2).
 {
 assert (CongaH Y Z1 Z2 Y Z2 Z1)
  by (apply (isosceles_congaH Y Z1 Z2);auto).

 apply congaH_permlr.
 apply (cong_5 Z1 Y X Z2 Y X).
  intro;apply H;Col.
  intro;apply H0;Col.
  apply congH_perms in H4;spliter; auto; try (intro; subst; Col).
  apply congH_perms in H3;spliter; auto; try (intro; subst; Col).
  assert (BetH Z1 X Z2) by (apply ncolH_distincts in H;
     apply ncolH_distincts in H0;apply congH_colH_betH;apply betH_expand in H2;spliter;auto).
  apply congaH_outH_congaH with Y Z2 Y Z1;auto using outH_trivial.
  apply ncolH_distincts in H;spliter;auto using outH_trivial.
  unfold outH. right;left;auto.
   apply ncolH_distincts in H0;spliter;auto using outH_trivial.
  unfold outH. right;left;auto using between_comm.
  }

assert (CongaH X Z1 Z2 X Z2 Z1)
  by (apply (isosceles_congaH X Z1 Z2);auto).
assert (CongaH Y Z1 Z2 Y Z2 Z1)
  by (apply (isosceles_congaH Y Z1 Z2);auto).
assert (CongaH X Z1 Y X Z2 Y).
  {
  apply th15 with Z2 Z1; auto;
  try solve[intro; apply H5; Col]; try solve[intro; apply H6; Col];
  try solve[intro; apply H; Col]; try solve[intro; apply H0; Col].
  elim (plane_separation X Y Z1 Z2); Col; intro HS; [left|right]; split; auto;
  destruct HS; split; auto.
  }
apply congaH_permlr.
apply (cong_5 Z1 Y X Z2 Y X);auto using congaH_permlr, congH_perms.
 intro;apply H;Col.
 intro;apply H0;Col.
 apply congH_perms in H4;spliter; auto; try (intro; subst; Col).
 apply congH_perms in H3;spliter; auto; try (intro; subst; Col).
Qed.

Lemma congaH_existence_congH :
  A B C O X P U V : Point,
       UV
       ¬ ColH P O X
       ¬ ColH A B C
        Y : Point, CongaH A B C X O Y same_side' P Y O X CongH O Y U V.
Proof.
intros.
assert (T:=ncolH_distincts A B C H1).
assert (T':=ncolH_distincts P O X H0).
spliter.
elim (hcong_4_existence A B C O X P); auto.
intros Yaux [HA HB].
assert (OYaux).
  {
  apply same_side_prime_not_colH in HB; destruct HB as [_ HFalse].
  intro; subst O; apply HFalse; Col.
  }
elim (out_construction O Yaux U V);auto.
intros Y [HC HD].
Y.
split.
apply congaH_outH_congaH with A C X Yaux;auto using outH_trivial.
split.
 elim (line_existence O X H3).
 intros l [HL1 HL2].
 assert (same_side Y Yaux l).
  {
   apply (out_same_side O Y Yaux);auto.
   apply (same_side_prime_not_colH P Yaux O X) in HB.
   spliter.
   apply outH_expand in HD.
   intro;apply H10.
   spliter.
   assert (ColH O X Y) by ( l;auto).
   ColHR.
   apply outH_sym;auto.
   apply outH_expand in HD;spliter;auto.
  }
  unfold same_side'.
  split;auto.
  intros.
  assert (EqL l0 l).
   apply line_uniqueness with O X;auto.
  rewrite H12.
  unfold same_side' in HB;spliter.
  specialize H14 with l.
  apply same_side_trans with Yaux;auto using same_side_comm.
assumption.
Qed.

Lemma th18_aux:
A B C A' B' C',
  ¬ ColH A B C
  ¬ ColH A' B' C'
  CongH A B A' B'
  CongH A C A' C'
  CongH B C B' C'
  CongaH B A C B' A' C'.
Proof.
intros.
assert (T:=ncolH_distincts A B C H).
assert (U:=ncolH_distincts A' B' C' H0).
spliter.
elim (congaH_existence_congH C A B A' C' B' A B);try solve [intuition Col].
intros B0 [HA [HB HC]].
elim (between_out B' C');auto.
intros P HP.
elim (congaH_existence_congH C A B A' C' P A B);try solve [intuition Col].
intros B'' [HA'' [HB'' HC'']].
assert (¬ ColH A' C' B0).
 intro.
 apply (same_side_prime_not_colH B' B0 A' C');intuition Col.
assert (¬ ColH A' C' B'').
 intro.
 apply (same_side_prime_not_colH P B'' A' C');intuition Col.
assert (CongH B C B0 C').
 {
  apply (th12 A B C A' B0 C').
  intuition Col.
  intuition Col.
  apply ncolH_expand in H10; spliter.
  auto using congH_sym.
  auto.
  apply congaH_permlr;auto.
 }
assert (CongH B C B'' C').
 {
  apply (th12 A B C A' B'' C').
  intuition Col.
  intuition Col.
  apply ncolH_expand in H11; spliter.
  auto using congH_sym.
  auto.
  apply congaH_permlr;auto.
 }
assert (HA'B'' : A' B'') by (apply ncolH_expand in H11; spliter; auto).
assert (HA'B0 : A' B0) by (apply <