Library GeoCoq.Elements.OriginalProofs.proposition_42B
Require Export GeoCoq.Elements.OriginalProofs.proposition_42.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_42B :
∀ B C D E J K R a b c e,
Triangle a b c → Midpoint b e c → nCol J D K → Midpoint B E C → Cong E C e c → nCol R E C →
∃ X Z, PG X E C Z ∧ EF a b e c X E C Z ∧ CongA C E X J D K ∧ OS R X E C.
Proof.
intros.
assert ((BetS B E C ∧ Cong B E E C)) by (conclude_def Midpoint ).
assert ((BetS b e c ∧ Cong b e e c)) by (conclude_def Midpoint ).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (nCol a b c) by (conclude_def Triangle ).
assert (nCol a c b) by (forward_using lemma_NCorder).
assert (nCol E C R) by (forward_using lemma_NCorder).
assert (Col B E C) by (conclude_def Col ).
assert (Col E C B) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col E C C) by (conclude_def Col ).
assert (nCol B C R) by (conclude lemma_NChelper).
rename_H H;let Tf:=fresh in
assert (Tf:∃ P H, (Out B C H ∧ CongA P B H a b c ∧ OS P R B C)) by (conclude proposition_23C);destruct Tf as [P[H]];spliter.
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (neq b c) by (forward_using lemma_NCdistinct).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out B C C) by (conclude lemma_ray4).
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong E C B E) by (conclude lemma_congruencesymmetric).
assert (Cong E C e c) by (conclude lemma_congruencetransitive).
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong e c b e) by (conclude lemma_congruencesymmetric).
assert (Cong B E b e) by (conclude lemma_congruencetransitive).
assert (Cong B C b c) by (conclude lemma_sumofparts).
assert (CongA a b c P B H) by (conclude lemma_equalanglessymmetric).
assert (Out B H C) by (conclude lemma_ray5).
assert (nCol B C P) by (conclude_def OS ).
assert (neq B P) by (forward_using lemma_NCdistinct).
assert (nCol a b c) by (conclude_def Triangle ).
assert (neq b a) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ A, (Out B P A ∧ Cong B A b a)) by (conclude lemma_layoff);destruct Tf as [A];spliter.
assert (CongA a b c A B C) by (conclude lemma_equalangleshelper).
assert (CongA A B C a b c) by (conclude lemma_equalanglessymmetric).
assert (nCol A B C) by (conclude lemma_equalanglesNC).
assert (Triangle A B C) by (conclude_def Triangle ).
assert (Cong A C a c) by (conclude proposition_04).
assert (Cong A B a b) by (forward_using lemma_congruenceflip).
assert (Cong_3 A B C a b c) by (conclude_def Cong_3 ).
assert (ET A B C a b c) by (conclude axiom_congruentequal).
assert (Cong C A c a) by (forward_using lemma_congruenceflip).
assert (Cong E A e a) by (conclude lemma_interior5).
assert (Cong A E a e) by (forward_using lemma_congruenceflip).
assert (Cong E B e b) by (forward_using lemma_congruenceflip).
assert (Col B E C) by (conclude_def Col ).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (nCol B C A) by (forward_using lemma_NCorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (neq B E) by (forward_using lemma_betweennotequal).
assert (nCol B E A) by (conclude lemma_NChelper).
assert (nCol A E B) by (forward_using lemma_NCorder).
assert (Triangle A E B) by (conclude_def Triangle ).
assert (Col b e c) by (conclude_def Col ).
assert (Col b c e) by (forward_using lemma_collinearorder).
assert (nCol b c a) by (forward_using lemma_NCorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col b c b) by (conclude_def Col ).
assert (neq b e) by (forward_using lemma_betweennotequal).
assert (nCol b e a) by (conclude lemma_NChelper).
assert (nCol a e b) by (forward_using lemma_NCorder).
assert (Triangle a e b) by (conclude_def Triangle ).
assert (Cong_3 A E B a e b) by (conclude_def Cong_3 ).
assert (ET A E B a e b) by (conclude axiom_congruentequal).
assert (Col C B E) by (forward_using lemma_collinearorder).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col C B C) by (conclude_def Col ).
assert (neq E C) by (forward_using lemma_betweennotequal).
assert (neq C E) by (conclude lemma_inequalitysymmetric).
assert (nCol C E A) by (conclude lemma_NChelper).
assert (nCol A E C) by (forward_using lemma_NCorder).
assert (Triangle A E C) by (conclude_def Triangle ).
assert (Col c b e) by (forward_using lemma_collinearorder).
assert (nCol c b a) by (forward_using lemma_NCorder).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (Col c b c) by (conclude_def Col ).
assert (neq e c) by (forward_using lemma_betweennotequal).
assert (neq c e) by (conclude lemma_inequalitysymmetric).
assert (nCol c e a) by (conclude lemma_NChelper).
assert (nCol a e c) by (forward_using lemma_NCorder).
assert (Triangle a e c) by (conclude_def Triangle ).
assert (Cong_3 A E C a e c) by (conclude_def Cong_3 ).
assert (ET A E C a e c) by (conclude axiom_congruentequal).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col A E E) by (conclude_def Col ).
assert (TS B A E C) by (conclude_def TS ).
assert (eq e e) by (conclude cn_equalityreflexive).
assert (Col a e e) by (conclude_def Col ).
assert (TS b a e c) by (conclude_def TS ).
assert (EF A B E C a b e c) by (conclude axiom_paste3).
assert (EF a b e c A B E C) by (conclude axiom_EFsymmetric).
let Tf:=fresh in
assert (Tf:∃ F G, (PG F E C G ∧ EF A B E C F E C G ∧ CongA C E F J D K ∧ Col F G A)) by (conclude proposition_42);destruct Tf as [F[G]];spliter.
assert (EF a b e c F E C G) by (conclude axiom_EFtransitive).
assert (OS R P B C) by (forward_using lemma_samesidesymmetric).
assert (Col B B C) by (conclude_def Col ).
assert (OS R A B C) by (conclude lemma_sameside2).
assert (OS R A C B) by (conclude lemma_samesideflip).
assert (OS R A C E) by (conclude lemma_samesidecollinear).
assert (OS A R C E) by (forward_using lemma_samesidesymmetric).
assert (OS A R E C) by (conclude lemma_samesideflip).
assert (Col G F A) by (forward_using lemma_collinearorder).
assert (Par F G E C) by (conclude_def PG ).
assert (Par E C F G) by (conclude lemma_parallelsymmetric).
assert (Par E C G F) by (forward_using lemma_parallelflip).
assert (OS R F E C).
by cases on (eq A F ∨ neq A F).
{
assert (OS R A E C) by (conclude lemma_samesideflip).
assert (OS R F E C) by (conclude cn_equalitysub).
close.
}
{
assert (Par E C A F) by (conclude lemma_collinearparallel).
assert (Par E C F A) by (forward_using lemma_parallelflip).
assert (TP E C F A) by (conclude lemma_paralleldef2B).
assert (OS F A E C) by (conclude_def TP ).
assert (OS F R E C) by (conclude lemma_samesidetransitive).
assert (OS R F E C) by (forward_using lemma_samesidesymmetric).
close.
}
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_42B :
∀ B C D E J K R a b c e,
Triangle a b c → Midpoint b e c → nCol J D K → Midpoint B E C → Cong E C e c → nCol R E C →
∃ X Z, PG X E C Z ∧ EF a b e c X E C Z ∧ CongA C E X J D K ∧ OS R X E C.
Proof.
intros.
assert ((BetS B E C ∧ Cong B E E C)) by (conclude_def Midpoint ).
assert ((BetS b e c ∧ Cong b e e c)) by (conclude_def Midpoint ).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (nCol a b c) by (conclude_def Triangle ).
assert (nCol a c b) by (forward_using lemma_NCorder).
assert (nCol E C R) by (forward_using lemma_NCorder).
assert (Col B E C) by (conclude_def Col ).
assert (Col E C B) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col E C C) by (conclude_def Col ).
assert (nCol B C R) by (conclude lemma_NChelper).
rename_H H;let Tf:=fresh in
assert (Tf:∃ P H, (Out B C H ∧ CongA P B H a b c ∧ OS P R B C)) by (conclude proposition_23C);destruct Tf as [P[H]];spliter.
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (neq b c) by (forward_using lemma_NCdistinct).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out B C C) by (conclude lemma_ray4).
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong E C B E) by (conclude lemma_congruencesymmetric).
assert (Cong E C e c) by (conclude lemma_congruencetransitive).
assert (Cong B E e c) by (conclude lemma_congruencetransitive).
assert (Cong e c b e) by (conclude lemma_congruencesymmetric).
assert (Cong B E b e) by (conclude lemma_congruencetransitive).
assert (Cong B C b c) by (conclude lemma_sumofparts).
assert (CongA a b c P B H) by (conclude lemma_equalanglessymmetric).
assert (Out B H C) by (conclude lemma_ray5).
assert (nCol B C P) by (conclude_def OS ).
assert (neq B P) by (forward_using lemma_NCdistinct).
assert (nCol a b c) by (conclude_def Triangle ).
assert (neq b a) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ A, (Out B P A ∧ Cong B A b a)) by (conclude lemma_layoff);destruct Tf as [A];spliter.
assert (CongA a b c A B C) by (conclude lemma_equalangleshelper).
assert (CongA A B C a b c) by (conclude lemma_equalanglessymmetric).
assert (nCol A B C) by (conclude lemma_equalanglesNC).
assert (Triangle A B C) by (conclude_def Triangle ).
assert (Cong A C a c) by (conclude proposition_04).
assert (Cong A B a b) by (forward_using lemma_congruenceflip).
assert (Cong_3 A B C a b c) by (conclude_def Cong_3 ).
assert (ET A B C a b c) by (conclude axiom_congruentequal).
assert (Cong C A c a) by (forward_using lemma_congruenceflip).
assert (Cong E A e a) by (conclude lemma_interior5).
assert (Cong A E a e) by (forward_using lemma_congruenceflip).
assert (Cong E B e b) by (forward_using lemma_congruenceflip).
assert (Col B E C) by (conclude_def Col ).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (nCol B C A) by (forward_using lemma_NCorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (neq B E) by (forward_using lemma_betweennotequal).
assert (nCol B E A) by (conclude lemma_NChelper).
assert (nCol A E B) by (forward_using lemma_NCorder).
assert (Triangle A E B) by (conclude_def Triangle ).
assert (Col b e c) by (conclude_def Col ).
assert (Col b c e) by (forward_using lemma_collinearorder).
assert (nCol b c a) by (forward_using lemma_NCorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col b c b) by (conclude_def Col ).
assert (neq b e) by (forward_using lemma_betweennotequal).
assert (nCol b e a) by (conclude lemma_NChelper).
assert (nCol a e b) by (forward_using lemma_NCorder).
assert (Triangle a e b) by (conclude_def Triangle ).
assert (Cong_3 A E B a e b) by (conclude_def Cong_3 ).
assert (ET A E B a e b) by (conclude axiom_congruentequal).
assert (Col C B E) by (forward_using lemma_collinearorder).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col C B C) by (conclude_def Col ).
assert (neq E C) by (forward_using lemma_betweennotequal).
assert (neq C E) by (conclude lemma_inequalitysymmetric).
assert (nCol C E A) by (conclude lemma_NChelper).
assert (nCol A E C) by (forward_using lemma_NCorder).
assert (Triangle A E C) by (conclude_def Triangle ).
assert (Col c b e) by (forward_using lemma_collinearorder).
assert (nCol c b a) by (forward_using lemma_NCorder).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (Col c b c) by (conclude_def Col ).
assert (neq e c) by (forward_using lemma_betweennotequal).
assert (neq c e) by (conclude lemma_inequalitysymmetric).
assert (nCol c e a) by (conclude lemma_NChelper).
assert (nCol a e c) by (forward_using lemma_NCorder).
assert (Triangle a e c) by (conclude_def Triangle ).
assert (Cong_3 A E C a e c) by (conclude_def Cong_3 ).
assert (ET A E C a e c) by (conclude axiom_congruentequal).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col A E E) by (conclude_def Col ).
assert (TS B A E C) by (conclude_def TS ).
assert (eq e e) by (conclude cn_equalityreflexive).
assert (Col a e e) by (conclude_def Col ).
assert (TS b a e c) by (conclude_def TS ).
assert (EF A B E C a b e c) by (conclude axiom_paste3).
assert (EF a b e c A B E C) by (conclude axiom_EFsymmetric).
let Tf:=fresh in
assert (Tf:∃ F G, (PG F E C G ∧ EF A B E C F E C G ∧ CongA C E F J D K ∧ Col F G A)) by (conclude proposition_42);destruct Tf as [F[G]];spliter.
assert (EF a b e c F E C G) by (conclude axiom_EFtransitive).
assert (OS R P B C) by (forward_using lemma_samesidesymmetric).
assert (Col B B C) by (conclude_def Col ).
assert (OS R A B C) by (conclude lemma_sameside2).
assert (OS R A C B) by (conclude lemma_samesideflip).
assert (OS R A C E) by (conclude lemma_samesidecollinear).
assert (OS A R C E) by (forward_using lemma_samesidesymmetric).
assert (OS A R E C) by (conclude lemma_samesideflip).
assert (Col G F A) by (forward_using lemma_collinearorder).
assert (Par F G E C) by (conclude_def PG ).
assert (Par E C F G) by (conclude lemma_parallelsymmetric).
assert (Par E C G F) by (forward_using lemma_parallelflip).
assert (OS R F E C).
by cases on (eq A F ∨ neq A F).
{
assert (OS R A E C) by (conclude lemma_samesideflip).
assert (OS R F E C) by (conclude cn_equalitysub).
close.
}
{
assert (Par E C A F) by (conclude lemma_collinearparallel).
assert (Par E C F A) by (forward_using lemma_parallelflip).
assert (TP E C F A) by (conclude lemma_paralleldef2B).
assert (OS F A E C) by (conclude_def TP ).
assert (OS F R E C) by (conclude lemma_samesidetransitive).
assert (OS R F E C) by (forward_using lemma_samesidesymmetric).
close.
}
close.
Qed.
End Euclid.