# Library GeoCoq.Elements.OriginalProofs.proposition_30

Require Export GeoCoq.Elements.OriginalProofs.lemma_30helper.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossimpliesopposite.

Require Export GeoCoq.Elements.OriginalProofs.proposition_30A.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma proposition_30 :

∀ A B C D E F G H K,

Par A B E F → Par C D E F → BetS G H K → Col A B G → Col E F H → Col C D K → neq A G → neq E H → neq C K →

Par A B C D.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ b, (BetS A G b ∧ Cong G b A G)) by (conclude postulate_extension);destruct Tf as [b];spliter.

let Tf:=fresh in

assert (Tf:∃ f, (BetS E H f ∧ Cong H f E H)) by (conclude postulate_extension);destruct Tf as [f];spliter.

let Tf:=fresh in

assert (Tf:∃ d, (BetS C K d ∧ Cong K d C K)) by (conclude postulate_extension);destruct Tf as [d];spliter.

assert (nCol C D E) by (forward_using lemma_parallelNC).

assert (neq C D) by (forward_using lemma_NCdistinct).

assert (Col A G b) by (conclude_def Col ).

assert (Col G A b) by (forward_using lemma_collinearorder).

assert (Col G A B) by (forward_using lemma_collinearorder).

assert (neq G A) by (conclude lemma_inequalitysymmetric).

assert (Col A b B) by (conclude lemma_collinear4).

assert (Col B A b) by (forward_using lemma_collinearorder).

assert (Par E F A B) by (conclude lemma_parallelsymmetric).

assert (Par E F B A) by (forward_using lemma_parallelflip).

assert (neq A b) by (forward_using lemma_betweennotequal).

assert (neq b A) by (conclude lemma_inequalitysymmetric).

assert (Par E F b A) by (conclude lemma_collinearparallel).

assert (Par E F A b) by (forward_using lemma_parallelflip).

assert (Par A b E F) by (conclude lemma_parallelsymmetric).

assert (Col E H f) by (conclude_def Col ).

assert (Col H E f) by (forward_using lemma_collinearorder).

assert (Col H E F) by (forward_using lemma_collinearorder).

assert (neq H E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col F E f) by (forward_using lemma_collinearorder).

assert (neq E f) by (forward_using lemma_betweennotequal).

assert (neq f E) by (conclude lemma_inequalitysymmetric).

assert (Par A b F E) by (forward_using lemma_parallelflip).

assert (Par A b f E) by (conclude lemma_collinearparallel).

assert (Par A b E f) by (forward_using lemma_parallelflip).

assert (Col C K d) by (conclude_def Col ).

assert (Col K C d) by (forward_using lemma_collinearorder).

assert (Col K C D) by (forward_using lemma_collinearorder).

assert (neq K C) by (conclude lemma_inequalitysymmetric).

assert (Col C d D) by (conclude lemma_collinear4).

assert (Col D C d) by (forward_using lemma_collinearorder).

assert (Par E F C D) by (conclude lemma_parallelsymmetric).

assert (Par E F D C) by (forward_using lemma_parallelflip).

assert (neq C d) by (forward_using lemma_betweennotequal).

assert (neq d C) by (conclude lemma_inequalitysymmetric).

assert (Par E F d C) by (conclude lemma_collinearparallel).

assert (Par E F C d) by (forward_using lemma_parallelflip).

assert (Par C d E F) by (conclude lemma_parallelsymmetric).

assert (Par C d F E) by (forward_using lemma_parallelflip).

assert (Par C d f E) by (conclude lemma_collinearparallel).

assert (Par C d E f) by (forward_using lemma_parallelflip).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col E H H) by (conclude_def Col ).

assert (Col A b G) by (forward_using lemma_collinearorder).

assert (Col E f H) by (forward_using lemma_collinearorder).

assert (Col f E H) by (forward_using lemma_collinearorder).

assert (Par A b f E) by (forward_using lemma_parallelflip).

assert (Par A b H E) by (conclude lemma_collinearparallel).

assert (Par H E A b) by (conclude lemma_parallelsymmetric).

assert (Par E H b A) by (forward_using lemma_parallelflip).

assert (Col b A G) by (forward_using lemma_collinearorder).

assert (Par E H G A) by (conclude lemma_collinearparallel).

assert (Par E H A G) by (forward_using lemma_parallelflip).

assert (Par A G E H) by (conclude lemma_parallelsymmetric).

assert (Par C d f E) by (forward_using lemma_parallelflip).

assert (Col f E H) by (forward_using lemma_collinearorder).

assert (Par C d H E) by (conclude lemma_collinearparallel).

assert (Par H E C d) by (conclude lemma_parallelsymmetric).

assert (Par H E d C) by (forward_using lemma_parallelflip).

assert (Col C K d) by (conclude_def Col ).

assert (Col d C K) by (forward_using lemma_collinearorder).

assert (neq C K) by (forward_using lemma_betweennotequal).

assert (neq K C) by (conclude lemma_inequalitysymmetric).

assert (Par H E K C) by (conclude lemma_collinearparallel).

assert (Par E H C K) by (forward_using lemma_parallelflip).

assert (TP E H C K) by (conclude lemma_paralleldef2B).

assert (OS C K E H) by (conclude_def TP ).

assert (nCol E H K) by (forward_using lemma_parallelNC).

assert (BetS K H G) by (conclude axiom_betweennesssymmetry).

assert (TS K E H G) by (conclude_def TS ).

assert (TS C E H G) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q G ∧ Col E H Q ∧ nCol E H C)) by (conclude_def TS );destruct Tf as [Q];spliter.

assert (Par E f C d) by (conclude lemma_parallelsymmetric).

assert (TP E f C d) by (conclude lemma_paralleldef2B).

assert (OS C d E f) by (conclude_def TP ).

assert (OS d C E f) by (forward_using lemma_samesidesymmetric).

assert (Col E H f) by (conclude_def Col ).

assert (Col H E f) by (forward_using lemma_collinearorder).

assert (Col H E Q) by (forward_using lemma_collinearorder).

assert (Col E f Q) by (conclude lemma_collinear4).

assert (nCol C E f) by (forward_using lemma_parallelNC).

assert (nCol E f C) by (forward_using lemma_NCorder).

assert (TS C E f G) by (conclude_def TS ).

assert (TS d E f G) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ P, (BetS d P G ∧ Col E f P ∧ nCol E f d)) by (conclude_def TS );destruct Tf as [P];spliter.

assert (¬ ¬ (CR A f G H ∨ CR A E G H)).

{

intro.

assert (CR A E G H) by (conclude lemma_30helper).

contradict.

}

assert (¬ ¬ (CR C f K H ∨ CR C E K H)).

{

intro.

assert (CR C E K H) by (conclude lemma_30helper).

contradict.

}

assert (Col F E H) by (forward_using lemma_collinearorder).

assert (Col B A G) by (forward_using lemma_collinearorder).

assert (Par A B F E) by (forward_using lemma_parallelflip).

assert (Par A B H E) by (conclude lemma_collinearparallel).

assert (Par A B E H) by (forward_using lemma_parallelflip).

assert (Par E H A B) by (conclude lemma_parallelsymmetric).

assert (Par E H B A) by (forward_using lemma_parallelflip).

assert (Par E H G A) by (conclude lemma_collinearparallel).

assert (Par E H A G) by (forward_using lemma_parallelflip).

assert (Par A G E H) by (conclude lemma_parallelsymmetric).

assert (nCol A G H) by (forward_using lemma_parallelNC).

assert (Par C D F E) by (forward_using lemma_parallelflip).

assert (Par C D H E) by (conclude lemma_collinearparallel).

assert (Par C D E H) by (forward_using lemma_parallelflip).

assert (Par E H C D) by (conclude lemma_parallelsymmetric).

assert (Par E H D C) by (forward_using lemma_parallelflip).

assert (Col D C K) by (forward_using lemma_collinearorder).

assert (Par E H K C) by (conclude lemma_collinearparallel).

assert (Par E H C K) by (forward_using lemma_parallelflip).

assert (Par C K E H) by (conclude lemma_parallelsymmetric).

assert (nCol C K H) by (forward_using lemma_parallelNC).

assert (nCol K H C) by (forward_using lemma_NCorder).

assert (nCol E H K) by (forward_using lemma_parallelNC).

assert (Col E H f) by (conclude_def Col ).

assert (neq H f) by (forward_using lemma_betweennotequal).

assert (neq f H) by (conclude lemma_inequalitysymmetric).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col E H H) by (conclude_def Col ).

assert (nCol f H K) by (conclude lemma_NChelper).

assert (nCol K H f) by (forward_using lemma_NCorder).

assert (Col K H H) by (conclude_def Col ).

assert (Par A b C d).

by cases on (CR A f G H ∨ CR A E G H).

{

assert (TS A G H f) by (forward_using lemma_crossimpliesopposite).

assert (Par A b C d).

by cases on (CR C f K H ∨ CR C E K H).

{

assert (TS f H K C) by (forward_using lemma_crossimpliesopposite).

assert (Par A b C d) by (conclude proposition_30A).

close.

}

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M E ∧ BetS K M H)) by (conclude_def CR );destruct Tf as [M];spliter.

assert (Col K M H) by (conclude_def Col ).

assert (Col K H M) by (forward_using lemma_collinearorder).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (OS f C K H) by (conclude_def OS ).

assert (eq K K) by (conclude cn_equalityreflexive).

assert (Col K H K) by (conclude_def Col ).

assert (TS C K H d) by (conclude_def TS ).

assert (TS f K H d) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ m, (BetS f m d ∧ Col K H m ∧ nCol K H f)) by (conclude_def TS );destruct Tf as [m];spliter.

assert (Par f E C d) by (conclude lemma_parallelsymmetric).

assert (¬ Meet f E C d) by (conclude_def Par ).

assert (Col f H E) by (forward_using lemma_collinearorder).

assert (neq f E) by (forward_using lemma_betweennotequal).

assert (neq f H) by (conclude lemma_inequalitysymmetric).

assert (neq K d) by (forward_using lemma_betweennotequal).

assert (Col H K m) by (forward_using lemma_collinearorder).

assert (BetS H m K) by (conclude lemma_collinearbetween).

assert (BetS K m H) by (conclude axiom_betweennesssymmetry).

assert (BetS d m f) by (conclude axiom_betweennesssymmetry).

assert (CR d f K H) by (conclude_def CR ).

assert (nCol C K H) by (forward_using lemma_NCorder).

assert (Col C K d) by (conclude_def Col ).

assert (neq d K) by (conclude lemma_inequalitysymmetric).

assert (Col C K K) by (conclude_def Col ).

assert (nCol d K H) by (conclude lemma_NChelper).

assert (TS d H K f) by (forward_using lemma_crossimpliesopposite).

assert (Par d C E f) by (forward_using lemma_parallelflip).

assert (BetS d K C) by (conclude axiom_betweennesssymmetry).

assert (TS f H K d) by (conclude lemma_oppositesidesymmetric).

assert (Par A b d C) by (conclude proposition_30A).

assert (Par A b C d) by (forward_using lemma_parallelflip).

close.

}

close.

}

{

assert (Par A b C d).

by cases on (CR C f K H ∨ CR C E K H).

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M f ∧ BetS K M H)) by (conclude_def CR );destruct Tf as [M];spliter.

assert (Col K M H) by (conclude_def Col ).

assert (Col K H M) by (forward_using lemma_collinearorder).

assert (nCol K H E) by (forward_using lemma_NCorder).

assert (nCol K H C) by (forward_using lemma_NCorder).

assert (OS E C K H) by (conclude_def OS ).

assert (eq K K) by (conclude cn_equalityreflexive).

assert (Col K H K) by (conclude_def Col ).

assert (TS C K H d) by (conclude_def TS ).

assert (TS E K H d) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ m, (BetS E m d ∧ Col K H m ∧ nCol K H E)) by (conclude_def TS );destruct Tf as [m];spliter.

assert (Par E f C d) by (conclude lemma_parallelsymmetric).

assert (¬ Meet E f C d) by (conclude_def Par ).

assert (Col E H f) by (forward_using lemma_collinearorder).

assert (neq E f) by (forward_using lemma_betweennotequal).

assert (neq E H) by (conclude lemma_inequalitysymmetric).

assert (neq K d) by (forward_using lemma_betweennotequal).

assert (Col H K m) by (forward_using lemma_collinearorder).

assert (BetS H m K) by (conclude lemma_collinearbetween).

assert (BetS K m H) by (conclude axiom_betweennesssymmetry).

assert (BetS d m E) by (conclude axiom_betweennesssymmetry).

assert (CR d E K H) by (conclude_def CR ).

assert (nCol C K H) by (forward_using lemma_NCorder).

assert (Col C K d) by (conclude_def Col ).

assert (neq d K) by (conclude lemma_inequalitysymmetric).

assert (Col C K K) by (conclude_def Col ).

assert (nCol d K H) by (conclude lemma_NChelper).

assert (TS d H K E) by (forward_using lemma_crossimpliesopposite).

assert (Par d C f E) by (forward_using lemma_parallelflip).

assert (BetS d K C) by (conclude axiom_betweennesssymmetry).

assert (TS E H K d) by (conclude lemma_oppositesidesymmetric).

assert (TS A G H E) by (forward_using lemma_crossimpliesopposite).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (Par A b d C) by (conclude proposition_30A).

assert (Par A b C d) by (forward_using lemma_parallelflip).

close.

}

{

assert (TS C H K E) by (forward_using lemma_crossimpliesopposite).

assert (TS E H K C) by (conclude lemma_oppositesidesymmetric).

assert (TS A G H E) by (forward_using lemma_crossimpliesopposite).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (Par A b C d) by (conclude proposition_30A).

close.

}

close.

}

assert (Par A b d C) by (forward_using lemma_parallelflip).

assert (Col d C D) by (forward_using lemma_collinearorder).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (Par A b D C) by (conclude lemma_collinearparallel).

assert (Par A b C D) by (forward_using lemma_parallelflip).

assert (Par C D A b) by (conclude lemma_parallelsymmetric).

assert (Par C D b A) by (forward_using lemma_parallelflip).

assert (Col b A B) by (forward_using lemma_collinearorder).

assert (nCol A B E) by (forward_using lemma_parallelNC).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Par C D B A) by (conclude lemma_collinearparallel).

assert (Par C D A B) by (forward_using lemma_parallelflip).

assert (Par A B C D) by (conclude lemma_parallelsymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossimpliesopposite.

Require Export GeoCoq.Elements.OriginalProofs.proposition_30A.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma proposition_30 :

∀ A B C D E F G H K,

Par A B E F → Par C D E F → BetS G H K → Col A B G → Col E F H → Col C D K → neq A G → neq E H → neq C K →

Par A B C D.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ b, (BetS A G b ∧ Cong G b A G)) by (conclude postulate_extension);destruct Tf as [b];spliter.

let Tf:=fresh in

assert (Tf:∃ f, (BetS E H f ∧ Cong H f E H)) by (conclude postulate_extension);destruct Tf as [f];spliter.

let Tf:=fresh in

assert (Tf:∃ d, (BetS C K d ∧ Cong K d C K)) by (conclude postulate_extension);destruct Tf as [d];spliter.

assert (nCol C D E) by (forward_using lemma_parallelNC).

assert (neq C D) by (forward_using lemma_NCdistinct).

assert (Col A G b) by (conclude_def Col ).

assert (Col G A b) by (forward_using lemma_collinearorder).

assert (Col G A B) by (forward_using lemma_collinearorder).

assert (neq G A) by (conclude lemma_inequalitysymmetric).

assert (Col A b B) by (conclude lemma_collinear4).

assert (Col B A b) by (forward_using lemma_collinearorder).

assert (Par E F A B) by (conclude lemma_parallelsymmetric).

assert (Par E F B A) by (forward_using lemma_parallelflip).

assert (neq A b) by (forward_using lemma_betweennotequal).

assert (neq b A) by (conclude lemma_inequalitysymmetric).

assert (Par E F b A) by (conclude lemma_collinearparallel).

assert (Par E F A b) by (forward_using lemma_parallelflip).

assert (Par A b E F) by (conclude lemma_parallelsymmetric).

assert (Col E H f) by (conclude_def Col ).

assert (Col H E f) by (forward_using lemma_collinearorder).

assert (Col H E F) by (forward_using lemma_collinearorder).

assert (neq H E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col F E f) by (forward_using lemma_collinearorder).

assert (neq E f) by (forward_using lemma_betweennotequal).

assert (neq f E) by (conclude lemma_inequalitysymmetric).

assert (Par A b F E) by (forward_using lemma_parallelflip).

assert (Par A b f E) by (conclude lemma_collinearparallel).

assert (Par A b E f) by (forward_using lemma_parallelflip).

assert (Col C K d) by (conclude_def Col ).

assert (Col K C d) by (forward_using lemma_collinearorder).

assert (Col K C D) by (forward_using lemma_collinearorder).

assert (neq K C) by (conclude lemma_inequalitysymmetric).

assert (Col C d D) by (conclude lemma_collinear4).

assert (Col D C d) by (forward_using lemma_collinearorder).

assert (Par E F C D) by (conclude lemma_parallelsymmetric).

assert (Par E F D C) by (forward_using lemma_parallelflip).

assert (neq C d) by (forward_using lemma_betweennotequal).

assert (neq d C) by (conclude lemma_inequalitysymmetric).

assert (Par E F d C) by (conclude lemma_collinearparallel).

assert (Par E F C d) by (forward_using lemma_parallelflip).

assert (Par C d E F) by (conclude lemma_parallelsymmetric).

assert (Par C d F E) by (forward_using lemma_parallelflip).

assert (Par C d f E) by (conclude lemma_collinearparallel).

assert (Par C d E f) by (forward_using lemma_parallelflip).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col E H H) by (conclude_def Col ).

assert (Col A b G) by (forward_using lemma_collinearorder).

assert (Col E f H) by (forward_using lemma_collinearorder).

assert (Col f E H) by (forward_using lemma_collinearorder).

assert (Par A b f E) by (forward_using lemma_parallelflip).

assert (Par A b H E) by (conclude lemma_collinearparallel).

assert (Par H E A b) by (conclude lemma_parallelsymmetric).

assert (Par E H b A) by (forward_using lemma_parallelflip).

assert (Col b A G) by (forward_using lemma_collinearorder).

assert (Par E H G A) by (conclude lemma_collinearparallel).

assert (Par E H A G) by (forward_using lemma_parallelflip).

assert (Par A G E H) by (conclude lemma_parallelsymmetric).

assert (Par C d f E) by (forward_using lemma_parallelflip).

assert (Col f E H) by (forward_using lemma_collinearorder).

assert (Par C d H E) by (conclude lemma_collinearparallel).

assert (Par H E C d) by (conclude lemma_parallelsymmetric).

assert (Par H E d C) by (forward_using lemma_parallelflip).

assert (Col C K d) by (conclude_def Col ).

assert (Col d C K) by (forward_using lemma_collinearorder).

assert (neq C K) by (forward_using lemma_betweennotequal).

assert (neq K C) by (conclude lemma_inequalitysymmetric).

assert (Par H E K C) by (conclude lemma_collinearparallel).

assert (Par E H C K) by (forward_using lemma_parallelflip).

assert (TP E H C K) by (conclude lemma_paralleldef2B).

assert (OS C K E H) by (conclude_def TP ).

assert (nCol E H K) by (forward_using lemma_parallelNC).

assert (BetS K H G) by (conclude axiom_betweennesssymmetry).

assert (TS K E H G) by (conclude_def TS ).

assert (TS C E H G) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q G ∧ Col E H Q ∧ nCol E H C)) by (conclude_def TS );destruct Tf as [Q];spliter.

assert (Par E f C d) by (conclude lemma_parallelsymmetric).

assert (TP E f C d) by (conclude lemma_paralleldef2B).

assert (OS C d E f) by (conclude_def TP ).

assert (OS d C E f) by (forward_using lemma_samesidesymmetric).

assert (Col E H f) by (conclude_def Col ).

assert (Col H E f) by (forward_using lemma_collinearorder).

assert (Col H E Q) by (forward_using lemma_collinearorder).

assert (Col E f Q) by (conclude lemma_collinear4).

assert (nCol C E f) by (forward_using lemma_parallelNC).

assert (nCol E f C) by (forward_using lemma_NCorder).

assert (TS C E f G) by (conclude_def TS ).

assert (TS d E f G) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ P, (BetS d P G ∧ Col E f P ∧ nCol E f d)) by (conclude_def TS );destruct Tf as [P];spliter.

assert (¬ ¬ (CR A f G H ∨ CR A E G H)).

{

intro.

assert (CR A E G H) by (conclude lemma_30helper).

contradict.

}

assert (¬ ¬ (CR C f K H ∨ CR C E K H)).

{

intro.

assert (CR C E K H) by (conclude lemma_30helper).

contradict.

}

assert (Col F E H) by (forward_using lemma_collinearorder).

assert (Col B A G) by (forward_using lemma_collinearorder).

assert (Par A B F E) by (forward_using lemma_parallelflip).

assert (Par A B H E) by (conclude lemma_collinearparallel).

assert (Par A B E H) by (forward_using lemma_parallelflip).

assert (Par E H A B) by (conclude lemma_parallelsymmetric).

assert (Par E H B A) by (forward_using lemma_parallelflip).

assert (Par E H G A) by (conclude lemma_collinearparallel).

assert (Par E H A G) by (forward_using lemma_parallelflip).

assert (Par A G E H) by (conclude lemma_parallelsymmetric).

assert (nCol A G H) by (forward_using lemma_parallelNC).

assert (Par C D F E) by (forward_using lemma_parallelflip).

assert (Par C D H E) by (conclude lemma_collinearparallel).

assert (Par C D E H) by (forward_using lemma_parallelflip).

assert (Par E H C D) by (conclude lemma_parallelsymmetric).

assert (Par E H D C) by (forward_using lemma_parallelflip).

assert (Col D C K) by (forward_using lemma_collinearorder).

assert (Par E H K C) by (conclude lemma_collinearparallel).

assert (Par E H C K) by (forward_using lemma_parallelflip).

assert (Par C K E H) by (conclude lemma_parallelsymmetric).

assert (nCol C K H) by (forward_using lemma_parallelNC).

assert (nCol K H C) by (forward_using lemma_NCorder).

assert (nCol E H K) by (forward_using lemma_parallelNC).

assert (Col E H f) by (conclude_def Col ).

assert (neq H f) by (forward_using lemma_betweennotequal).

assert (neq f H) by (conclude lemma_inequalitysymmetric).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col E H H) by (conclude_def Col ).

assert (nCol f H K) by (conclude lemma_NChelper).

assert (nCol K H f) by (forward_using lemma_NCorder).

assert (Col K H H) by (conclude_def Col ).

assert (Par A b C d).

by cases on (CR A f G H ∨ CR A E G H).

{

assert (TS A G H f) by (forward_using lemma_crossimpliesopposite).

assert (Par A b C d).

by cases on (CR C f K H ∨ CR C E K H).

{

assert (TS f H K C) by (forward_using lemma_crossimpliesopposite).

assert (Par A b C d) by (conclude proposition_30A).

close.

}

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M E ∧ BetS K M H)) by (conclude_def CR );destruct Tf as [M];spliter.

assert (Col K M H) by (conclude_def Col ).

assert (Col K H M) by (forward_using lemma_collinearorder).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (OS f C K H) by (conclude_def OS ).

assert (eq K K) by (conclude cn_equalityreflexive).

assert (Col K H K) by (conclude_def Col ).

assert (TS C K H d) by (conclude_def TS ).

assert (TS f K H d) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ m, (BetS f m d ∧ Col K H m ∧ nCol K H f)) by (conclude_def TS );destruct Tf as [m];spliter.

assert (Par f E C d) by (conclude lemma_parallelsymmetric).

assert (¬ Meet f E C d) by (conclude_def Par ).

assert (Col f H E) by (forward_using lemma_collinearorder).

assert (neq f E) by (forward_using lemma_betweennotequal).

assert (neq f H) by (conclude lemma_inequalitysymmetric).

assert (neq K d) by (forward_using lemma_betweennotequal).

assert (Col H K m) by (forward_using lemma_collinearorder).

assert (BetS H m K) by (conclude lemma_collinearbetween).

assert (BetS K m H) by (conclude axiom_betweennesssymmetry).

assert (BetS d m f) by (conclude axiom_betweennesssymmetry).

assert (CR d f K H) by (conclude_def CR ).

assert (nCol C K H) by (forward_using lemma_NCorder).

assert (Col C K d) by (conclude_def Col ).

assert (neq d K) by (conclude lemma_inequalitysymmetric).

assert (Col C K K) by (conclude_def Col ).

assert (nCol d K H) by (conclude lemma_NChelper).

assert (TS d H K f) by (forward_using lemma_crossimpliesopposite).

assert (Par d C E f) by (forward_using lemma_parallelflip).

assert (BetS d K C) by (conclude axiom_betweennesssymmetry).

assert (TS f H K d) by (conclude lemma_oppositesidesymmetric).

assert (Par A b d C) by (conclude proposition_30A).

assert (Par A b C d) by (forward_using lemma_parallelflip).

close.

}

close.

}

{

assert (Par A b C d).

by cases on (CR C f K H ∨ CR C E K H).

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M f ∧ BetS K M H)) by (conclude_def CR );destruct Tf as [M];spliter.

assert (Col K M H) by (conclude_def Col ).

assert (Col K H M) by (forward_using lemma_collinearorder).

assert (nCol K H E) by (forward_using lemma_NCorder).

assert (nCol K H C) by (forward_using lemma_NCorder).

assert (OS E C K H) by (conclude_def OS ).

assert (eq K K) by (conclude cn_equalityreflexive).

assert (Col K H K) by (conclude_def Col ).

assert (TS C K H d) by (conclude_def TS ).

assert (TS E K H d) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ m, (BetS E m d ∧ Col K H m ∧ nCol K H E)) by (conclude_def TS );destruct Tf as [m];spliter.

assert (Par E f C d) by (conclude lemma_parallelsymmetric).

assert (¬ Meet E f C d) by (conclude_def Par ).

assert (Col E H f) by (forward_using lemma_collinearorder).

assert (neq E f) by (forward_using lemma_betweennotequal).

assert (neq E H) by (conclude lemma_inequalitysymmetric).

assert (neq K d) by (forward_using lemma_betweennotequal).

assert (Col H K m) by (forward_using lemma_collinearorder).

assert (BetS H m K) by (conclude lemma_collinearbetween).

assert (BetS K m H) by (conclude axiom_betweennesssymmetry).

assert (BetS d m E) by (conclude axiom_betweennesssymmetry).

assert (CR d E K H) by (conclude_def CR ).

assert (nCol C K H) by (forward_using lemma_NCorder).

assert (Col C K d) by (conclude_def Col ).

assert (neq d K) by (conclude lemma_inequalitysymmetric).

assert (Col C K K) by (conclude_def Col ).

assert (nCol d K H) by (conclude lemma_NChelper).

assert (TS d H K E) by (forward_using lemma_crossimpliesopposite).

assert (Par d C f E) by (forward_using lemma_parallelflip).

assert (BetS d K C) by (conclude axiom_betweennesssymmetry).

assert (TS E H K d) by (conclude lemma_oppositesidesymmetric).

assert (TS A G H E) by (forward_using lemma_crossimpliesopposite).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (Par A b d C) by (conclude proposition_30A).

assert (Par A b C d) by (forward_using lemma_parallelflip).

close.

}

{

assert (TS C H K E) by (forward_using lemma_crossimpliesopposite).

assert (TS E H K C) by (conclude lemma_oppositesidesymmetric).

assert (TS A G H E) by (forward_using lemma_crossimpliesopposite).

assert (BetS f H E) by (conclude axiom_betweennesssymmetry).

assert (Par A b C d) by (conclude proposition_30A).

close.

}

close.

}

assert (Par A b d C) by (forward_using lemma_parallelflip).

assert (Col d C D) by (forward_using lemma_collinearorder).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (Par A b D C) by (conclude lemma_collinearparallel).

assert (Par A b C D) by (forward_using lemma_parallelflip).

assert (Par C D A b) by (conclude lemma_parallelsymmetric).

assert (Par C D b A) by (forward_using lemma_parallelflip).

assert (Col b A B) by (forward_using lemma_collinearorder).

assert (nCol A B E) by (forward_using lemma_parallelNC).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Par C D B A) by (conclude lemma_collinearparallel).

assert (Par C D A B) by (forward_using lemma_parallelflip).

assert (Par A B C D) by (conclude lemma_parallelsymmetric).

close.

Qed.

End Euclid.