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.