Library GeoCoq.Elements.OriginalProofs.proposition_35A
Require Export GeoCoq.Elements.OriginalProofs.lemma_35helper.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ETreflexive.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_35A :
∀ A B C D E F,
PG A B C D → PG E B C F → BetS A D F → Col A E F →
EF A B C D E B C F.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
assert ((Par E B C F ∧ Par E F B C)) by (conclude_def PG ).
assert (Par A B D C) by (forward_using lemma_parallelflip).
assert (Par E B F C) by (forward_using lemma_parallelflip).
assert (Cong A D B C) by (forward_using proposition_34).
assert (Cong E F B C) by (forward_using proposition_34).
assert (Cong B C E F) by (conclude lemma_congruencesymmetric).
assert (Cong A D E F) by (conclude lemma_congruencetransitive).
assert (Cong E F F E) by (conclude cn_equalityreverse).
assert (Cong A D F E) by (conclude lemma_congruencetransitive).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Lt F E A F) by (conclude lemma_lessthancongruence2).
assert (Cong A F F A) by (conclude cn_equalityreverse).
assert (Lt F E F A) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ e, (BetS F e A ∧ Cong F e F E)) by (conclude_def Lt );destruct Tf as [e];spliter.
assert (neq F A) by (forward_using lemma_betweennotequal).
assert (Out F A e) by (conclude lemma_ray4).
assert (BetS A E F) by (conclude lemma_35helper).
assert (BetS F E A) by (conclude axiom_betweennesssymmetry).
assert (Out F A E) by (conclude lemma_ray4).
assert (eq e E) by (conclude lemma_layoffunique).
assert (BetS F E A) by (conclude cn_equalitysub).
assert (BetS A E F) by (conclude axiom_betweennesssymmetry).
assert (Cong A B D C) by (forward_using proposition_34).
assert (Par D C A B) by (conclude lemma_parallelsymmetric).
assert (BetS F D A) by (conclude axiom_betweennesssymmetry).
assert (TP A D B C) by (conclude lemma_paralleldef2B).
assert (OS B C A D) by (conclude_def TP ).
assert (OS C B D A) by (forward_using lemma_samesidesymmetric).
assert (CongA F D C D A B) by (conclude proposition_29C).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (neq F D) by (forward_using lemma_betweennotequal).
assert (neq D F) by (conclude lemma_inequalitysymmetric).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (¬ eq D C).
{
intro.
assert (Col A D C) by (conclude_def Col ).
contradict.
}
assert (neq C D) by (conclude lemma_inequalitysymmetric).
assert (¬ eq A D).
{
intro.
assert (Col A D C) by (conclude_def Col ).
contradict.
}
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (Out A B B) by (conclude lemma_ray4).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ ¬ (BetS A D E ∨ BetS A E D ∨ eq D E)).
{
intro.
assert (eq D E) by (eapply ( axiom_connectivity) with A F;auto).
contradict.
}
assert (Out A D E).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
assert (Out A D E) by (conclude lemma_ray4).
close.
}
{
assert (Out A D E) by (conclude lemma_ray4).
close.
}
{
assert (Out A D D) by (conclude lemma_ray4).
assert (Out A D E) by (conclude cn_equalitysub).
close.
}
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (CongA D A B D A B) by (conclude lemma_equalanglesreflexive).
assert (CongA D A B E A B) by (conclude lemma_equalangleshelper).
assert (CongA F D C E A B) by (conclude lemma_equalanglestransitive).
assert (Cong A B D C) by (conclude proposition_34).
assert (Cong D E E D) by (conclude cn_equalityreverse).
assert (Cong E D D E) by (conclude cn_equalityreverse).
assert (Cong A E D F).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
assert (BetS D E F) by (conclude lemma_3_6a).
assert (BetS F E D) by (conclude axiom_betweennesssymmetry).
assert (Cong A E F D) by (conclude lemma_sumofparts).
assert (Cong A E D F) by (forward_using lemma_congruenceflip).
close.
}
{
assert (BetS D E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D F) by (conclude lemma_3_6a).
assert (Cong D A E F) by (forward_using lemma_congruenceflip).
assert (Cong E A D F) by (conclude lemma_differenceofparts).
assert (Cong A E D F) by (forward_using lemma_congruenceflip).
close.
}
{
assert (Cong A E E F) by (conclude cn_equalitysub).
assert (Cong A E D F) by (conclude cn_equalitysub).
close.
}
assert (CongA E A B F D C) by (conclude lemma_equalanglessymmetric).
assert (nCol F D C) by (conclude lemma_equalanglesNC).
assert (Triangle F D C) by (conclude_def Triangle ).
assert (nCol E A B) by (conclude lemma_equalanglesNC).
assert (Triangle E A B) by (conclude_def Triangle ).
assert (Cong D F A E) by (conclude lemma_congruencesymmetric).
assert (Cong D C A B) by (conclude lemma_congruencesymmetric).
assert ((Cong F C E B ∧ CongA D F C A E B ∧ CongA D C F A B E)) by (conclude proposition_04).
assert (Cong F D E A) by (forward_using lemma_congruenceflip).
assert (Cong_3 F D C E A B) by (conclude_def Cong_3 ).
assert (ET F D C E A B) by (conclude axiom_congruentequal).
assert (EF A B C D E B C F).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M D)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (Col A D E) by (conclude_def Col ).
assert (Col A D A) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (nCol A E B) by (conclude lemma_NChelper).
assert (BetS B M D) by (conclude axiom_betweennesssymmetry).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS B H E ∧ BetS A M H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col A M H) by (conclude_def Col ).
assert (Col A M C) by (conclude_def Col ).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (neq M A) by (conclude lemma_inequalitysymmetric).
assert (Col M A H) by (forward_using lemma_collinearorder).
assert (Col M A C) by (forward_using lemma_collinearorder).
assert (Col A H C) by (conclude lemma_collinear4).
assert (BetS E H B) by (conclude axiom_betweennesssymmetry).
assert (Col E A A) by (conclude_def Col ).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (Col B C C) by (conclude_def Col ).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (¬ Meet E A C B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ q, (neq E A ∧ neq C B ∧ Col E A q ∧ Col C B q)) by (conclude_def Meet );destruct Tf as [q];spliter.
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Col A E q) by (forward_using lemma_collinearorder).
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col E A q) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D q) by (conclude lemma_collinear4).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Col A C H) by (forward_using lemma_collinearorder).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (Col E A A) by (conclude_def Col ).
assert (Col C C B) by (conclude_def Col ).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (BetS A H C) by (conclude lemma_collinearbetween).
assert (BetS C H A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D A) by (conclude axiom_betweennesssymmetry).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (Col A D E) by (conclude_def Col ).
assert (nCol A E C) by (conclude lemma_NChelper).
assert (nCol C A E) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ G, (BetS C G D ∧ BetS E G H)) by (conclude postulate_Pasch_inner);destruct Tf as [G];spliter.
assert (BetS E G B) by (conclude lemma_3_6b).
assert (Triangle A E B) by (conclude_def Triangle ).
assert (BetS E G B) by (conclude lemma_3_6b).
assert (Col E G B) by (conclude_def Col ).
assert (¬ Col D E G).
{
intro.
assert (Col G E D) by (forward_using lemma_collinearorder).
assert (Col G E B) by (forward_using lemma_collinearorder).
assert (neq E G) by (forward_using lemma_betweennotequal).
assert (neq G E) by (conclude lemma_inequalitysymmetric).
assert (Col E D B) by (conclude lemma_collinear4).
assert (Col B C B) by (conclude_def Col ).
assert (Col E D A) by (forward_using lemma_collinearorder).
assert (Col E D D) by (conclude_def Col ).
assert (neq D E) by (forward_using lemma_betweennotequal).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (Col A D B) by (conclude lemma_collinear5).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Triangle D E G) by (conclude_def Triangle ).
assert (ET D E G D E G) by (conclude lemma_ETreflexive).
assert (ET D E G E D G) by (forward_using axiom_ETpermutation).
assert (ET F D C A E B) by (forward_using axiom_ETpermutation).
assert (ET A E B F D C) by (conclude axiom_ETsymmetric).
assert (BetS B G E) by (conclude axiom_betweennesssymmetry).
assert (BetS D E F) by (conclude lemma_3_6a).
assert (BetS F E D) by (conclude axiom_betweennesssymmetry).
assert (EF A D G B F E G C) by (conclude axiom_cutoff1).
assert (nCol E G D) by (forward_using lemma_NCorder).
assert (eq G G) by (conclude cn_equalityreflexive).
assert (Col E G G) by (conclude_def Col ).
assert (neq G B) by (forward_using lemma_betweennotequal).
assert (neq B G) by (conclude lemma_inequalitysymmetric).
assert (nCol B G D) by (conclude lemma_NChelper).
assert (nCol D G B) by (forward_using lemma_NCorder).
assert (Col C G D) by (conclude_def Col ).
assert (Col D G C) by (forward_using lemma_collinearorder).
assert (Col D G G) by (conclude_def Col ).
assert (neq C G) by (forward_using lemma_betweennotequal).
assert (nCol C G B) by (conclude lemma_NChelper).
assert (nCol G C B) by (forward_using lemma_NCorder).
assert (Triangle G C B) by (conclude_def Triangle ).
assert (ET G C B G C B) by (conclude lemma_ETreflexive).
assert (ET G C B G B C) by (forward_using axiom_ETpermutation).
assert (BetS D G C) by (conclude axiom_betweennesssymmetry).
assert (EF A D C B F E B C) by (conclude axiom_paste2).
assert (EF A D C B E B C F) by (forward_using axiom_EFpermutation).
assert (EF E B C F A D C B) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C D) by (forward_using axiom_EFpermutation).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
{
assert (ET E A B F D C) by (conclude axiom_ETsymmetric).
assert (ET E A B D F C) by (forward_using axiom_ETpermutation).
assert (EF B E D C B E D C) by (conclude axiom_EFreflexive).
assert (EF B E D C C D E B) by (forward_using axiom_EFpermutation).
assert (EF C D E B B E D C) by (conclude axiom_EFsymmetric).
assert (BetS D E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D F) by (conclude lemma_3_6a).
assert (EF C D A B B E F C) by (conclude axiom_paste2).
assert (EF C D A B E B C F) by (forward_using axiom_EFpermutation).
assert (EF E B C F C D A B) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C D) by (forward_using axiom_EFpermutation).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
{
assert (ET F D C B E A) by (forward_using axiom_ETpermutation).
assert (ET B E A F D C) by (conclude axiom_ETsymmetric).
assert (ET B E A C D F) by (forward_using axiom_ETpermutation).
assert (nCol D B C) by (forward_using lemma_parallelNC).
assert (nCol E B C) by (conclude cn_equalitysub).
assert (nCol B E C) by (forward_using lemma_NCorder).
assert (Triangle B E C) by (conclude_def Triangle ).
assert (ET B E C B E C) by (conclude lemma_ETreflexive).
assert (ET B E C C E B) by (forward_using axiom_ETpermutation).
assert (ET B E C C D B) by (conclude cn_equalitysub).
assert (PG A B C E) by (conclude cn_equalitysub).
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M E)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS E M B) by (conclude axiom_betweennesssymmetry).
assert (Col E M B) by (conclude_def Col ).
assert (Col B E M) by (forward_using lemma_collinearorder).
assert (Par A E B C) by (conclude_def PG ).
assert (nCol A E B) by (forward_using lemma_parallelNC).
assert (nCol B E A) by (forward_using lemma_NCorder).
assert (TS A B E C) by (conclude_def TS ).
assert (PG D B C F) by (conclude cn_equalitysub).
assert (Par D F B C) by (conclude_def PG ).
assert (nCol D F C) by (forward_using lemma_parallelNC).
assert (nCol C D F) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ m, (BetS D m C ∧ BetS B m F)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.
assert (BetS F m B) by (conclude axiom_betweennesssymmetry).
assert (Col D m C) by (conclude_def Col ).
assert (Col C D m) by (forward_using lemma_collinearorder).
assert (TS F C D B) by (conclude_def TS ).
assert (EF B A E C C F D B) by (conclude axiom_paste3).
assert (EF B A E C D B C F) by (forward_using axiom_EFpermutation).
assert (EF B A E C E B C F) by (conclude cn_equalitysub).
assert (EF E B C F B A E C) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C E) by (forward_using axiom_EFpermutation).
assert (EF E B C F A B C D) by (conclude cn_equalitysub).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ETreflexive.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_35A :
∀ A B C D E F,
PG A B C D → PG E B C F → BetS A D F → Col A E F →
EF A B C D E B C F.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
assert ((Par E B C F ∧ Par E F B C)) by (conclude_def PG ).
assert (Par A B D C) by (forward_using lemma_parallelflip).
assert (Par E B F C) by (forward_using lemma_parallelflip).
assert (Cong A D B C) by (forward_using proposition_34).
assert (Cong E F B C) by (forward_using proposition_34).
assert (Cong B C E F) by (conclude lemma_congruencesymmetric).
assert (Cong A D E F) by (conclude lemma_congruencetransitive).
assert (Cong E F F E) by (conclude cn_equalityreverse).
assert (Cong A D F E) by (conclude lemma_congruencetransitive).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Lt F E A F) by (conclude lemma_lessthancongruence2).
assert (Cong A F F A) by (conclude cn_equalityreverse).
assert (Lt F E F A) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ e, (BetS F e A ∧ Cong F e F E)) by (conclude_def Lt );destruct Tf as [e];spliter.
assert (neq F A) by (forward_using lemma_betweennotequal).
assert (Out F A e) by (conclude lemma_ray4).
assert (BetS A E F) by (conclude lemma_35helper).
assert (BetS F E A) by (conclude axiom_betweennesssymmetry).
assert (Out F A E) by (conclude lemma_ray4).
assert (eq e E) by (conclude lemma_layoffunique).
assert (BetS F E A) by (conclude cn_equalitysub).
assert (BetS A E F) by (conclude axiom_betweennesssymmetry).
assert (Cong A B D C) by (forward_using proposition_34).
assert (Par D C A B) by (conclude lemma_parallelsymmetric).
assert (BetS F D A) by (conclude axiom_betweennesssymmetry).
assert (TP A D B C) by (conclude lemma_paralleldef2B).
assert (OS B C A D) by (conclude_def TP ).
assert (OS C B D A) by (forward_using lemma_samesidesymmetric).
assert (CongA F D C D A B) by (conclude proposition_29C).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (neq F D) by (forward_using lemma_betweennotequal).
assert (neq D F) by (conclude lemma_inequalitysymmetric).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (¬ eq D C).
{
intro.
assert (Col A D C) by (conclude_def Col ).
contradict.
}
assert (neq C D) by (conclude lemma_inequalitysymmetric).
assert (¬ eq A D).
{
intro.
assert (Col A D C) by (conclude_def Col ).
contradict.
}
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (Out A B B) by (conclude lemma_ray4).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ ¬ (BetS A D E ∨ BetS A E D ∨ eq D E)).
{
intro.
assert (eq D E) by (eapply ( axiom_connectivity) with A F;auto).
contradict.
}
assert (Out A D E).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
assert (Out A D E) by (conclude lemma_ray4).
close.
}
{
assert (Out A D E) by (conclude lemma_ray4).
close.
}
{
assert (Out A D D) by (conclude lemma_ray4).
assert (Out A D E) by (conclude cn_equalitysub).
close.
}
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (CongA D A B D A B) by (conclude lemma_equalanglesreflexive).
assert (CongA D A B E A B) by (conclude lemma_equalangleshelper).
assert (CongA F D C E A B) by (conclude lemma_equalanglestransitive).
assert (Cong A B D C) by (conclude proposition_34).
assert (Cong D E E D) by (conclude cn_equalityreverse).
assert (Cong E D D E) by (conclude cn_equalityreverse).
assert (Cong A E D F).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
assert (BetS D E F) by (conclude lemma_3_6a).
assert (BetS F E D) by (conclude axiom_betweennesssymmetry).
assert (Cong A E F D) by (conclude lemma_sumofparts).
assert (Cong A E D F) by (forward_using lemma_congruenceflip).
close.
}
{
assert (BetS D E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D F) by (conclude lemma_3_6a).
assert (Cong D A E F) by (forward_using lemma_congruenceflip).
assert (Cong E A D F) by (conclude lemma_differenceofparts).
assert (Cong A E D F) by (forward_using lemma_congruenceflip).
close.
}
{
assert (Cong A E E F) by (conclude cn_equalitysub).
assert (Cong A E D F) by (conclude cn_equalitysub).
close.
}
assert (CongA E A B F D C) by (conclude lemma_equalanglessymmetric).
assert (nCol F D C) by (conclude lemma_equalanglesNC).
assert (Triangle F D C) by (conclude_def Triangle ).
assert (nCol E A B) by (conclude lemma_equalanglesNC).
assert (Triangle E A B) by (conclude_def Triangle ).
assert (Cong D F A E) by (conclude lemma_congruencesymmetric).
assert (Cong D C A B) by (conclude lemma_congruencesymmetric).
assert ((Cong F C E B ∧ CongA D F C A E B ∧ CongA D C F A B E)) by (conclude proposition_04).
assert (Cong F D E A) by (forward_using lemma_congruenceflip).
assert (Cong_3 F D C E A B) by (conclude_def Cong_3 ).
assert (ET F D C E A B) by (conclude axiom_congruentequal).
assert (EF A B C D E B C F).
by cases on (BetS A D E ∨ BetS A E D ∨ eq D E).
{
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M D)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (Col A D E) by (conclude_def Col ).
assert (Col A D A) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (nCol A E B) by (conclude lemma_NChelper).
assert (BetS B M D) by (conclude axiom_betweennesssymmetry).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS B H E ∧ BetS A M H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col A M H) by (conclude_def Col ).
assert (Col A M C) by (conclude_def Col ).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (neq M A) by (conclude lemma_inequalitysymmetric).
assert (Col M A H) by (forward_using lemma_collinearorder).
assert (Col M A C) by (forward_using lemma_collinearorder).
assert (Col A H C) by (conclude lemma_collinear4).
assert (BetS E H B) by (conclude axiom_betweennesssymmetry).
assert (Col E A A) by (conclude_def Col ).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (Col B C C) by (conclude_def Col ).
assert (nCol A B C) by (forward_using lemma_parallelNC).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (¬ Meet E A C B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ q, (neq E A ∧ neq C B ∧ Col E A q ∧ Col C B q)) by (conclude_def Meet );destruct Tf as [q];spliter.
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Col A E q) by (forward_using lemma_collinearorder).
assert (Col A D E) by (conclude_def Col ).
assert (Col E A D) by (forward_using lemma_collinearorder).
assert (Col E A q) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D q) by (conclude lemma_collinear4).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Col A C H) by (forward_using lemma_collinearorder).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (Col E A A) by (conclude_def Col ).
assert (Col C C B) by (conclude_def Col ).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (BetS A H C) by (conclude lemma_collinearbetween).
assert (BetS C H A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D A) by (conclude axiom_betweennesssymmetry).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (Col A D E) by (conclude_def Col ).
assert (nCol A E C) by (conclude lemma_NChelper).
assert (nCol C A E) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ G, (BetS C G D ∧ BetS E G H)) by (conclude postulate_Pasch_inner);destruct Tf as [G];spliter.
assert (BetS E G B) by (conclude lemma_3_6b).
assert (Triangle A E B) by (conclude_def Triangle ).
assert (BetS E G B) by (conclude lemma_3_6b).
assert (Col E G B) by (conclude_def Col ).
assert (¬ Col D E G).
{
intro.
assert (Col G E D) by (forward_using lemma_collinearorder).
assert (Col G E B) by (forward_using lemma_collinearorder).
assert (neq E G) by (forward_using lemma_betweennotequal).
assert (neq G E) by (conclude lemma_inequalitysymmetric).
assert (Col E D B) by (conclude lemma_collinear4).
assert (Col B C B) by (conclude_def Col ).
assert (Col E D A) by (forward_using lemma_collinearorder).
assert (Col E D D) by (conclude_def Col ).
assert (neq D E) by (forward_using lemma_betweennotequal).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (Col A D B) by (conclude lemma_collinear5).
assert (Meet A D B C) by (conclude_def Meet ).
contradict.
}
assert (Triangle D E G) by (conclude_def Triangle ).
assert (ET D E G D E G) by (conclude lemma_ETreflexive).
assert (ET D E G E D G) by (forward_using axiom_ETpermutation).
assert (ET F D C A E B) by (forward_using axiom_ETpermutation).
assert (ET A E B F D C) by (conclude axiom_ETsymmetric).
assert (BetS B G E) by (conclude axiom_betweennesssymmetry).
assert (BetS D E F) by (conclude lemma_3_6a).
assert (BetS F E D) by (conclude axiom_betweennesssymmetry).
assert (EF A D G B F E G C) by (conclude axiom_cutoff1).
assert (nCol E G D) by (forward_using lemma_NCorder).
assert (eq G G) by (conclude cn_equalityreflexive).
assert (Col E G G) by (conclude_def Col ).
assert (neq G B) by (forward_using lemma_betweennotequal).
assert (neq B G) by (conclude lemma_inequalitysymmetric).
assert (nCol B G D) by (conclude lemma_NChelper).
assert (nCol D G B) by (forward_using lemma_NCorder).
assert (Col C G D) by (conclude_def Col ).
assert (Col D G C) by (forward_using lemma_collinearorder).
assert (Col D G G) by (conclude_def Col ).
assert (neq C G) by (forward_using lemma_betweennotequal).
assert (nCol C G B) by (conclude lemma_NChelper).
assert (nCol G C B) by (forward_using lemma_NCorder).
assert (Triangle G C B) by (conclude_def Triangle ).
assert (ET G C B G C B) by (conclude lemma_ETreflexive).
assert (ET G C B G B C) by (forward_using axiom_ETpermutation).
assert (BetS D G C) by (conclude axiom_betweennesssymmetry).
assert (EF A D C B F E B C) by (conclude axiom_paste2).
assert (EF A D C B E B C F) by (forward_using axiom_EFpermutation).
assert (EF E B C F A D C B) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C D) by (forward_using axiom_EFpermutation).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
{
assert (ET E A B F D C) by (conclude axiom_ETsymmetric).
assert (ET E A B D F C) by (forward_using axiom_ETpermutation).
assert (EF B E D C B E D C) by (conclude axiom_EFreflexive).
assert (EF B E D C C D E B) by (forward_using axiom_EFpermutation).
assert (EF C D E B B E D C) by (conclude axiom_EFsymmetric).
assert (BetS D E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E D F) by (conclude lemma_3_6a).
assert (EF C D A B B E F C) by (conclude axiom_paste2).
assert (EF C D A B E B C F) by (forward_using axiom_EFpermutation).
assert (EF E B C F C D A B) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C D) by (forward_using axiom_EFpermutation).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
{
assert (ET F D C B E A) by (forward_using axiom_ETpermutation).
assert (ET B E A F D C) by (conclude axiom_ETsymmetric).
assert (ET B E A C D F) by (forward_using axiom_ETpermutation).
assert (nCol D B C) by (forward_using lemma_parallelNC).
assert (nCol E B C) by (conclude cn_equalitysub).
assert (nCol B E C) by (forward_using lemma_NCorder).
assert (Triangle B E C) by (conclude_def Triangle ).
assert (ET B E C B E C) by (conclude lemma_ETreflexive).
assert (ET B E C C E B) by (forward_using axiom_ETpermutation).
assert (ET B E C C D B) by (conclude cn_equalitysub).
assert (PG A B C E) by (conclude cn_equalitysub).
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M E)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS E M B) by (conclude axiom_betweennesssymmetry).
assert (Col E M B) by (conclude_def Col ).
assert (Col B E M) by (forward_using lemma_collinearorder).
assert (Par A E B C) by (conclude_def PG ).
assert (nCol A E B) by (forward_using lemma_parallelNC).
assert (nCol B E A) by (forward_using lemma_NCorder).
assert (TS A B E C) by (conclude_def TS ).
assert (PG D B C F) by (conclude cn_equalitysub).
assert (Par D F B C) by (conclude_def PG ).
assert (nCol D F C) by (forward_using lemma_parallelNC).
assert (nCol C D F) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ m, (BetS D m C ∧ BetS B m F)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.
assert (BetS F m B) by (conclude axiom_betweennesssymmetry).
assert (Col D m C) by (conclude_def Col ).
assert (Col C D m) by (forward_using lemma_collinearorder).
assert (TS F C D B) by (conclude_def TS ).
assert (EF B A E C C F D B) by (conclude axiom_paste3).
assert (EF B A E C D B C F) by (forward_using axiom_EFpermutation).
assert (EF B A E C E B C F) by (conclude cn_equalitysub).
assert (EF E B C F B A E C) by (conclude axiom_EFsymmetric).
assert (EF E B C F A B C E) by (forward_using axiom_EFpermutation).
assert (EF E B C F A B C D) by (conclude cn_equalitysub).
assert (EF A B C D E B C F) by (conclude axiom_EFsymmetric).
close.
}
close.
Qed.
End Euclid.