Library GeoCoq.Elements.OriginalProofs.proposition_44A
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGrotate.
Require Export GeoCoq.Elements.OriginalProofs.proposition_33B.
Require Export GeoCoq.Elements.OriginalProofs.proposition_30.
Require Export GeoCoq.Elements.OriginalProofs.lemma_diagonalsbisect.
Require Export GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelbetween.
Require Export GeoCoq.Elements.OriginalProofs.proposition_43.
Require Export GeoCoq.Elements.OriginalProofs.proposition_43B.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_44A :
∀ A B D E F G J N,
PG B E F G → CongA E B G J D N → BetS A B E →
∃ X Y, PG A B X Y ∧ CongA A B X J D N ∧ EF B E F G Y X B A ∧ BetS G B X.
Proof.
intros.
assert (PG E F G B) by (conclude lemma_PGrotate).
assert (PG F G B E) by (conclude lemma_PGrotate).
assert (PG G B E F) by (conclude lemma_PGrotate).
assert (Par G F B E) by (conclude_def PG ).
assert (nCol G B E) by (forward_using lemma_parallelNC).
assert (neq G B) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ q, (BetS G B q ∧ Cong B q G B)) by (conclude postulate_extension);destruct Tf as [q];spliter.
assert (nCol E B G) by (forward_using lemma_NCorder).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col E B B) by (conclude_def Col ).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (nCol A B G) by (conclude lemma_NChelper).
assert (Col G B q) by (conclude_def Col ).
assert (nCol G B A) by (forward_using lemma_NCorder).
assert (neq G q) by (forward_using lemma_betweennotequal).
assert (neq q G) by (conclude lemma_inequalitysymmetric).
assert (eq G G) by (conclude cn_equalityreflexive).
assert (Col G B G) by (conclude_def Col ).
assert (nCol q G A) by (conclude lemma_NChelper).
assert (nCol G q A) by (forward_using lemma_NCorder).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H h T, (BetS H A h ∧ CongA h A B A B G ∧ CongA h A B G B A ∧ CongA B A h G B A ∧ CongA H A B A B q ∧ CongA H A B q B A ∧ CongA B A H q B A ∧ Par H h G q ∧ Cong H A B q ∧ Cong A h G B ∧ Cong A T T B ∧ Cong H T T q ∧ Cong G T T h ∧ BetS H T q ∧ BetS G T h ∧ BetS A T B)) by (conclude proposition_31);destruct Tf as [H[h[T]]];spliter.
assert (Par H h q G) by (forward_using lemma_parallelflip).
assert (Col G B q) by (conclude_def Col ).
assert (Col q G B) by (forward_using lemma_collinearorder).
assert (neq B G) by (forward_using lemma_NCdistinct).
assert (Par H h B G) by (conclude lemma_collinearparallel).
assert (Par H h G B) by (forward_using lemma_parallelflip).
assert (Par G B H h) by (conclude lemma_parallelsymmetric).
assert (Par G B h H) by (forward_using lemma_parallelflip).
assert (Col H A h) by (conclude_def Col ).
assert (Col h H A) by (forward_using lemma_collinearorder).
assert (neq H A) by (forward_using lemma_betweennotequal).
assert (neq A H) by (conclude lemma_inequalitysymmetric).
assert (Par G B A H) by (conclude lemma_collinearparallel).
assert (Par G B H A) by (forward_using lemma_parallelflip).
assert (Par H A G B) by (conclude lemma_parallelsymmetric).
assert (Cong H A G B) by (conclude lemma_congruencetransitive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (Col A T B) by (conclude_def Col ).
assert (Col A B T) by (forward_using lemma_collinearorder).
assert (nCol B H A) by (forward_using lemma_parallelNC).
assert (nCol A B H) by (forward_using lemma_NCorder).
assert (nCol H A B) by (forward_using lemma_parallelNC).
assert (nCol A B H) by (forward_using lemma_NCorder).
assert (OS H G A B) by (conclude_def OS ).
assert ((Par H G A B ∧ Cong H G A B)) by (conclude proposition_33B).
assert (Par A B H G) by (conclude lemma_parallelsymmetric).
assert (Par A B G H) by (forward_using lemma_parallelflip).
assert ((Par G B E F ∧ Par G F B E)) by (conclude_def PG ).
assert (Par G F E B) by (forward_using lemma_parallelflip).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (Par G F A B) by (conclude lemma_collinearparallel).
assert (Par A B G F) by (conclude lemma_parallelsymmetric).
assert (Col G H F) by (conclude lemma_Playfair).
assert (Par H A B G) by (forward_using lemma_parallelflip).
assert (Par G B F E) by (forward_using lemma_parallelflip).
assert (Par F E G B) by (conclude lemma_parallelsymmetric).
assert (PG H A B G) by (conclude_def PG ).
let Tf:=fresh in
assert (Tf:∃ j, (BetS H j B ∧ BetS A j G)) by (conclude lemma_diagonalsmeet);destruct Tf as [j];spliter.
let Tf:=fresh in
assert (Tf:∃ k, (BetS G k E ∧ BetS B k F)) by (conclude lemma_diagonalsmeet);destruct Tf as [k];spliter.
assert (BetS E B A) by (conclude axiom_betweennesssymmetry).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col F E E) by (conclude_def Col ).
assert (Col G B B) by (conclude_def Col ).
assert (Col H A A) by (conclude_def Col ).
assert (nCol F E B) by (forward_using lemma_parallelNC).
assert (neq F E) by (forward_using lemma_NCdistinct).
assert (neq G B) by (forward_using lemma_NCdistinct).
assert (nCol H A G) by (forward_using lemma_parallelNC).
assert (neq H A) by (forward_using lemma_NCdistinct).
assert (Par H A F E) by (conclude proposition_30).
assert (Cong G B F E) by (forward_using proposition_34).
assert (Cong H A F E) by (conclude lemma_congruencetransitive).
assert (Par G F B E) by (conclude_def PG ).
assert (Par H G A B) by (conclude_def PG ).
assert (Par B E G F) by (conclude lemma_parallelsymmetric).
assert (Par A B H G) by (conclude lemma_parallelsymmetric).
assert (TP B E G F) by (conclude lemma_paralleldef2B).
assert (TP A B H G) by (conclude lemma_paralleldef2B).
assert (OS G F B E) by (conclude_def TP ).
assert (OS H G A B) by (conclude_def TP ).
assert (Col A B E) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (OS H G A E) by (conclude lemma_samesidecollinear).
assert (OS G F E B) by (conclude lemma_samesideflip).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (OS G F E A) by (conclude lemma_samesidecollinear).
assert (OS G F A E) by (conclude lemma_samesideflip).
assert (OS H F A E) by (conclude lemma_samesidetransitive).
assert (Par H F A E) by (conclude proposition_33B).
assert (Par H A E F) by (forward_using lemma_parallelflip).
assert (PG H A E F) by (conclude_def PG ).
assert (nCol H F E) by (forward_using lemma_parallelNC).
assert (nCol E F H) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ t, (Midpoint H t E ∧ Midpoint A t F)) by (conclude lemma_diagonalsbisect);destruct Tf as [t];spliter.
assert ((BetS H t E ∧ Cong H t t E)) by (conclude_def Midpoint ).
assert ((BetS A t F ∧ Cong A t t F)) by (conclude_def Midpoint ).
assert (Cong A t F t) by (forward_using lemma_congruenceflip).
assert (Cong H t E t) by (forward_using lemma_congruenceflip).
assert (Cong t A t F) by (forward_using lemma_congruenceflip).
assert (nCol H E F) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ K, (BetS H B K ∧ BetS F E K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.
assert (Col F E K) by (conclude_def Col ).
assert (Col E F K) by (forward_using lemma_collinearorder).
assert (neq F K) by (forward_using lemma_betweennotequal).
assert (neq K F) by (conclude lemma_inequalitysymmetric).
assert (Par H A K F) by (conclude lemma_collinearparallel).
assert (Par H A F K) by (forward_using lemma_parallelflip).
assert (Par F K H A) by (conclude lemma_parallelsymmetric).
assert (Par F K A H) by (forward_using lemma_parallelflip).
assert (eq H H) by (conclude cn_equalityreflexive).
assert (Col A H H) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ L, (PG H L K F ∧ Col A H L)) by (conclude lemma_triangletoparallelogram);destruct Tf as [L];spliter.
assert (Par H L K F) by (conclude_def PG ).
assert (nCol L K F) by (forward_using lemma_parallelNC).
assert (neq L K) by (forward_using lemma_NCdistinct).
assert (neq K L) by (conclude lemma_inequalitysymmetric).
assert (Par G B E F) by (conclude_def PG ).
assert (Par G B F E) by (forward_using lemma_parallelflip).
assert (Col F E E) by (conclude_def Col ).
assert (Col F E K) by (conclude_def Col ).
assert (neq E K) by (forward_using lemma_betweennotequal).
assert (Par G B E K) by (conclude lemma_collinearparallel2).
assert (Par E K G B) by (conclude lemma_parallelsymmetric).
assert (Col G B B) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ M, (PG B M K E ∧ Col G B M)) by (conclude lemma_triangletoparallelogram);destruct Tf as [M];spliter.
assert (PG L K F H) by (conclude lemma_PGrotate).
assert (PG K L H F) by (conclude lemma_PGflip).
assert (PG L H F K) by (conclude lemma_PGrotate).
assert (PG H F K L) by (conclude lemma_PGrotate).
assert (PG A H G B) by (conclude lemma_PGflip).
assert (Par A H G B) by (conclude_def PG ).
assert (eq K K) by (conclude cn_equalityreflexive).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Par B E M K) by (conclude_def PG ).
assert (Par M K B E) by (conclude lemma_parallelsymmetric).
assert (Par K M E B) by (forward_using lemma_parallelflip).
assert (Par G F B E) by (conclude_def PG ).
assert (nCol E M K) by (forward_using lemma_parallelNC).
assert (nCol B E K) by (forward_using lemma_parallelNC).
assert (nCol G F B) by (forward_using lemma_parallelNC).
assert (Par M K B E) by (forward_using lemma_parallelflip).
assert (Par G F B E) by (forward_using lemma_parallelflip).
assert (BetS K E F) by (conclude axiom_betweennesssymmetry).
assert (Col M K K) by (conclude_def Col ).
assert (Col B E E) by (conclude_def Col ).
assert (Col G F F) by (conclude_def Col ).
assert (neq M K) by (forward_using lemma_NCdistinct).
assert (neq B E) by (forward_using lemma_NCdistinct).
assert (neq G F) by (forward_using lemma_NCdistinct).
assert (Par M K G F) by (conclude proposition_30).
assert (Par K M F G) by (forward_using lemma_parallelflip).
assert (Par F G K M) by (conclude lemma_parallelsymmetric).
assert (Par H F L K) by (conclude_def PG ).
assert (Par L K H F) by (conclude lemma_parallelsymmetric).
assert (Par K L H F) by (forward_using lemma_parallelflip).
assert (Col H F G) by (forward_using lemma_collinearorder).
assert (Par K L G F) by (conclude lemma_collinearparallel).
assert (Par K L F G) by (forward_using lemma_parallelflip).
assert (Par F G K L) by (conclude lemma_parallelsymmetric).
assert (Col K M L) by (conclude lemma_Playfair).
assert (Col M K L) by (forward_using lemma_collinearorder).
assert (Par B E M K) by (conclude_def PG ).
assert (neq L K) by (conclude lemma_inequalitysymmetric).
assert (Par B E L K) by (conclude lemma_collinearparallel).
assert (Par L K B E) by (conclude lemma_parallelsymmetric).
assert (Par L K E B) by (forward_using lemma_parallelflip).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (Par L K A B) by (conclude lemma_collinearparallel).
assert (Par A B L K) by (conclude lemma_parallelsymmetric).
assert (Par A B K L) by (forward_using lemma_parallelflip).
assert (BetS K B H) by (conclude axiom_betweennesssymmetry).
assert (Col L A H) by (forward_using lemma_collinearorder).
assert (BetS L A H) by (conclude lemma_parallelbetween).
assert (BetS H A L) by (conclude axiom_betweennesssymmetry).
assert (Par H A G B) by (forward_using lemma_parallelflip).
assert (nCol B M K) by (forward_using lemma_parallelNC).
assert (neq M B) by (forward_using lemma_NCdistinct).
assert (Par H A M B) by (conclude lemma_collinearparallel).
assert (Par M B H A) by (conclude lemma_parallelsymmetric).
assert (Par M B A H) by (forward_using lemma_parallelflip).
assert (Col A H L) by (forward_using lemma_collinearorder).
assert (Par H L K F) by (conclude_def PG ).
assert (nCol H L K) by (forward_using lemma_parallelNC).
assert (neq L H) by (forward_using lemma_NCdistinct).
assert (Par M B L H) by (conclude lemma_collinearparallel).
assert (Par M B H L) by (forward_using lemma_parallelflip).
assert (Col L M K) by (forward_using lemma_collinearorder).
assert (BetS L M K) by (conclude lemma_parallelbetween).
assert (Par G B E F) by (conclude_def PG ).
assert (Col F E K) by (conclude_def Col ).
assert (Col E F K) by (forward_using lemma_collinearorder).
assert (neq F K) by (forward_using lemma_betweennotequal).
assert (neq K F) by (conclude lemma_inequalitysymmetric).
assert (Par G B K F) by (conclude lemma_collinearparallel).
assert (Col F G H) by (forward_using lemma_collinearorder).
assert (BetS F G H) by (conclude lemma_parallelbetween).
assert (BetS H G F) by (conclude axiom_betweennesssymmetry).
assert (PG A B G H) by (conclude lemma_PGrotate).
assert (PG B G H A) by (conclude lemma_PGrotate).
assert (PG G H A B) by (conclude lemma_PGrotate).
assert (PG M K E B) by (conclude lemma_PGrotate).
assert (PG K E B M) by (conclude lemma_PGrotate).
assert (PG E B M K) by (conclude lemma_PGrotate).
assert (EF B E F G L M B A) by (conclude proposition_43).
assert (PG A H G B) by (conclude lemma_PGflip).
assert (PG M B E K) by (conclude lemma_PGflip).
assert (PG A B M L) by (conclude proposition_43B).
assert (Col H G F) by (forward_using lemma_collinearorder).
assert (neq H F) by (forward_using lemma_betweennotequal).
assert (neq L K) by (forward_using lemma_betweennotequal).
assert (neq H G) by (forward_using lemma_betweennotequal).
assert (neq M K) by (forward_using lemma_betweennotequal).
assert (Par H F L K) by (conclude_def PG ).
assert (¬ Meet H F L K)
by (unfold Par in H251;decompose [ex and] H251;auto).
assert (Col G M B) by (forward_using lemma_collinearorder).
assert (BetS G B M) by (conclude lemma_collinearbetween).
assert (CongA A B M G B E) by (conclude proposition_15).
assert (CongA G B E E B G) by (conclude lemma_ABCequalsCBA).
assert (CongA A B M E B G) by (conclude lemma_equalanglestransitive).
assert (CongA A B M J D N) by (conclude lemma_equalanglestransitive).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.proposition_33B.
Require Export GeoCoq.Elements.OriginalProofs.proposition_30.
Require Export GeoCoq.Elements.OriginalProofs.lemma_diagonalsbisect.
Require Export GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelbetween.
Require Export GeoCoq.Elements.OriginalProofs.proposition_43.
Require Export GeoCoq.Elements.OriginalProofs.proposition_43B.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_44A :
∀ A B D E F G J N,
PG B E F G → CongA E B G J D N → BetS A B E →
∃ X Y, PG A B X Y ∧ CongA A B X J D N ∧ EF B E F G Y X B A ∧ BetS G B X.
Proof.
intros.
assert (PG E F G B) by (conclude lemma_PGrotate).
assert (PG F G B E) by (conclude lemma_PGrotate).
assert (PG G B E F) by (conclude lemma_PGrotate).
assert (Par G F B E) by (conclude_def PG ).
assert (nCol G B E) by (forward_using lemma_parallelNC).
assert (neq G B) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ q, (BetS G B q ∧ Cong B q G B)) by (conclude postulate_extension);destruct Tf as [q];spliter.
assert (nCol E B G) by (forward_using lemma_NCorder).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col E B B) by (conclude_def Col ).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (nCol A B G) by (conclude lemma_NChelper).
assert (Col G B q) by (conclude_def Col ).
assert (nCol G B A) by (forward_using lemma_NCorder).
assert (neq G q) by (forward_using lemma_betweennotequal).
assert (neq q G) by (conclude lemma_inequalitysymmetric).
assert (eq G G) by (conclude cn_equalityreflexive).
assert (Col G B G) by (conclude_def Col ).
assert (nCol q G A) by (conclude lemma_NChelper).
assert (nCol G q A) by (forward_using lemma_NCorder).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H h T, (BetS H A h ∧ CongA h A B A B G ∧ CongA h A B G B A ∧ CongA B A h G B A ∧ CongA H A B A B q ∧ CongA H A B q B A ∧ CongA B A H q B A ∧ Par H h G q ∧ Cong H A B q ∧ Cong A h G B ∧ Cong A T T B ∧ Cong H T T q ∧ Cong G T T h ∧ BetS H T q ∧ BetS G T h ∧ BetS A T B)) by (conclude proposition_31);destruct Tf as [H[h[T]]];spliter.
assert (Par H h q G) by (forward_using lemma_parallelflip).
assert (Col G B q) by (conclude_def Col ).
assert (Col q G B) by (forward_using lemma_collinearorder).
assert (neq B G) by (forward_using lemma_NCdistinct).
assert (Par H h B G) by (conclude lemma_collinearparallel).
assert (Par H h G B) by (forward_using lemma_parallelflip).
assert (Par G B H h) by (conclude lemma_parallelsymmetric).
assert (Par G B h H) by (forward_using lemma_parallelflip).
assert (Col H A h) by (conclude_def Col ).
assert (Col h H A) by (forward_using lemma_collinearorder).
assert (neq H A) by (forward_using lemma_betweennotequal).
assert (neq A H) by (conclude lemma_inequalitysymmetric).
assert (Par G B A H) by (conclude lemma_collinearparallel).
assert (Par G B H A) by (forward_using lemma_parallelflip).
assert (Par H A G B) by (conclude lemma_parallelsymmetric).
assert (Cong H A G B) by (conclude lemma_congruencetransitive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (Col A T B) by (conclude_def Col ).
assert (Col A B T) by (forward_using lemma_collinearorder).
assert (nCol B H A) by (forward_using lemma_parallelNC).
assert (nCol A B H) by (forward_using lemma_NCorder).
assert (nCol H A B) by (forward_using lemma_parallelNC).
assert (nCol A B H) by (forward_using lemma_NCorder).
assert (OS H G A B) by (conclude_def OS ).
assert ((Par H G A B ∧ Cong H G A B)) by (conclude proposition_33B).
assert (Par A B H G) by (conclude lemma_parallelsymmetric).
assert (Par A B G H) by (forward_using lemma_parallelflip).
assert ((Par G B E F ∧ Par G F B E)) by (conclude_def PG ).
assert (Par G F E B) by (forward_using lemma_parallelflip).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (Par G F A B) by (conclude lemma_collinearparallel).
assert (Par A B G F) by (conclude lemma_parallelsymmetric).
assert (Col G H F) by (conclude lemma_Playfair).
assert (Par H A B G) by (forward_using lemma_parallelflip).
assert (Par G B F E) by (forward_using lemma_parallelflip).
assert (Par F E G B) by (conclude lemma_parallelsymmetric).
assert (PG H A B G) by (conclude_def PG ).
let Tf:=fresh in
assert (Tf:∃ j, (BetS H j B ∧ BetS A j G)) by (conclude lemma_diagonalsmeet);destruct Tf as [j];spliter.
let Tf:=fresh in
assert (Tf:∃ k, (BetS G k E ∧ BetS B k F)) by (conclude lemma_diagonalsmeet);destruct Tf as [k];spliter.
assert (BetS E B A) by (conclude axiom_betweennesssymmetry).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col F E E) by (conclude_def Col ).
assert (Col G B B) by (conclude_def Col ).
assert (Col H A A) by (conclude_def Col ).
assert (nCol F E B) by (forward_using lemma_parallelNC).
assert (neq F E) by (forward_using lemma_NCdistinct).
assert (neq G B) by (forward_using lemma_NCdistinct).
assert (nCol H A G) by (forward_using lemma_parallelNC).
assert (neq H A) by (forward_using lemma_NCdistinct).
assert (Par H A F E) by (conclude proposition_30).
assert (Cong G B F E) by (forward_using proposition_34).
assert (Cong H A F E) by (conclude lemma_congruencetransitive).
assert (Par G F B E) by (conclude_def PG ).
assert (Par H G A B) by (conclude_def PG ).
assert (Par B E G F) by (conclude lemma_parallelsymmetric).
assert (Par A B H G) by (conclude lemma_parallelsymmetric).
assert (TP B E G F) by (conclude lemma_paralleldef2B).
assert (TP A B H G) by (conclude lemma_paralleldef2B).
assert (OS G F B E) by (conclude_def TP ).
assert (OS H G A B) by (conclude_def TP ).
assert (Col A B E) by (conclude_def Col ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (OS H G A E) by (conclude lemma_samesidecollinear).
assert (OS G F E B) by (conclude lemma_samesideflip).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (OS G F E A) by (conclude lemma_samesidecollinear).
assert (OS G F A E) by (conclude lemma_samesideflip).
assert (OS H F A E) by (conclude lemma_samesidetransitive).
assert (Par H F A E) by (conclude proposition_33B).
assert (Par H A E F) by (forward_using lemma_parallelflip).
assert (PG H A E F) by (conclude_def PG ).
assert (nCol H F E) by (forward_using lemma_parallelNC).
assert (nCol E F H) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ t, (Midpoint H t E ∧ Midpoint A t F)) by (conclude lemma_diagonalsbisect);destruct Tf as [t];spliter.
assert ((BetS H t E ∧ Cong H t t E)) by (conclude_def Midpoint ).
assert ((BetS A t F ∧ Cong A t t F)) by (conclude_def Midpoint ).
assert (Cong A t F t) by (forward_using lemma_congruenceflip).
assert (Cong H t E t) by (forward_using lemma_congruenceflip).
assert (Cong t A t F) by (forward_using lemma_congruenceflip).
assert (nCol H E F) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ K, (BetS H B K ∧ BetS F E K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.
assert (Col F E K) by (conclude_def Col ).
assert (Col E F K) by (forward_using lemma_collinearorder).
assert (neq F K) by (forward_using lemma_betweennotequal).
assert (neq K F) by (conclude lemma_inequalitysymmetric).
assert (Par H A K F) by (conclude lemma_collinearparallel).
assert (Par H A F K) by (forward_using lemma_parallelflip).
assert (Par F K H A) by (conclude lemma_parallelsymmetric).
assert (Par F K A H) by (forward_using lemma_parallelflip).
assert (eq H H) by (conclude cn_equalityreflexive).
assert (Col A H H) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ L, (PG H L K F ∧ Col A H L)) by (conclude lemma_triangletoparallelogram);destruct Tf as [L];spliter.
assert (Par H L K F) by (conclude_def PG ).
assert (nCol L K F) by (forward_using lemma_parallelNC).
assert (neq L K) by (forward_using lemma_NCdistinct).
assert (neq K L) by (conclude lemma_inequalitysymmetric).
assert (Par G B E F) by (conclude_def PG ).
assert (Par G B F E) by (forward_using lemma_parallelflip).
assert (Col F E E) by (conclude_def Col ).
assert (Col F E K) by (conclude_def Col ).
assert (neq E K) by (forward_using lemma_betweennotequal).
assert (Par G B E K) by (conclude lemma_collinearparallel2).
assert (Par E K G B) by (conclude lemma_parallelsymmetric).
assert (Col G B B) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:∃ M, (PG B M K E ∧ Col G B M)) by (conclude lemma_triangletoparallelogram);destruct Tf as [M];spliter.
assert (PG L K F H) by (conclude lemma_PGrotate).
assert (PG K L H F) by (conclude lemma_PGflip).
assert (PG L H F K) by (conclude lemma_PGrotate).
assert (PG H F K L) by (conclude lemma_PGrotate).
assert (PG A H G B) by (conclude lemma_PGflip).
assert (Par A H G B) by (conclude_def PG ).
assert (eq K K) by (conclude cn_equalityreflexive).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Par B E M K) by (conclude_def PG ).
assert (Par M K B E) by (conclude lemma_parallelsymmetric).
assert (Par K M E B) by (forward_using lemma_parallelflip).
assert (Par G F B E) by (conclude_def PG ).
assert (nCol E M K) by (forward_using lemma_parallelNC).
assert (nCol B E K) by (forward_using lemma_parallelNC).
assert (nCol G F B) by (forward_using lemma_parallelNC).
assert (Par M K B E) by (forward_using lemma_parallelflip).
assert (Par G F B E) by (forward_using lemma_parallelflip).
assert (BetS K E F) by (conclude axiom_betweennesssymmetry).
assert (Col M K K) by (conclude_def Col ).
assert (Col B E E) by (conclude_def Col ).
assert (Col G F F) by (conclude_def Col ).
assert (neq M K) by (forward_using lemma_NCdistinct).
assert (neq B E) by (forward_using lemma_NCdistinct).
assert (neq G F) by (forward_using lemma_NCdistinct).
assert (Par M K G F) by (conclude proposition_30).
assert (Par K M F G) by (forward_using lemma_parallelflip).
assert (Par F G K M) by (conclude lemma_parallelsymmetric).
assert (Par H F L K) by (conclude_def PG ).
assert (Par L K H F) by (conclude lemma_parallelsymmetric).
assert (Par K L H F) by (forward_using lemma_parallelflip).
assert (Col H F G) by (forward_using lemma_collinearorder).
assert (Par K L G F) by (conclude lemma_collinearparallel).
assert (Par K L F G) by (forward_using lemma_parallelflip).
assert (Par F G K L) by (conclude lemma_parallelsymmetric).
assert (Col K M L) by (conclude lemma_Playfair).
assert (Col M K L) by (forward_using lemma_collinearorder).
assert (Par B E M K) by (conclude_def PG ).
assert (neq L K) by (conclude lemma_inequalitysymmetric).
assert (Par B E L K) by (conclude lemma_collinearparallel).
assert (Par L K B E) by (conclude lemma_parallelsymmetric).
assert (Par L K E B) by (forward_using lemma_parallelflip).
assert (Col A B E) by (conclude_def Col ).
assert (Col E B A) by (forward_using lemma_collinearorder).
assert (Par L K A B) by (conclude lemma_collinearparallel).
assert (Par A B L K) by (conclude lemma_parallelsymmetric).
assert (Par A B K L) by (forward_using lemma_parallelflip).
assert (BetS K B H) by (conclude axiom_betweennesssymmetry).
assert (Col L A H) by (forward_using lemma_collinearorder).
assert (BetS L A H) by (conclude lemma_parallelbetween).
assert (BetS H A L) by (conclude axiom_betweennesssymmetry).
assert (Par H A G B) by (forward_using lemma_parallelflip).
assert (nCol B M K) by (forward_using lemma_parallelNC).
assert (neq M B) by (forward_using lemma_NCdistinct).
assert (Par H A M B) by (conclude lemma_collinearparallel).
assert (Par M B H A) by (conclude lemma_parallelsymmetric).
assert (Par M B A H) by (forward_using lemma_parallelflip).
assert (Col A H L) by (forward_using lemma_collinearorder).
assert (Par H L K F) by (conclude_def PG ).
assert (nCol H L K) by (forward_using lemma_parallelNC).
assert (neq L H) by (forward_using lemma_NCdistinct).
assert (Par M B L H) by (conclude lemma_collinearparallel).
assert (Par M B H L) by (forward_using lemma_parallelflip).
assert (Col L M K) by (forward_using lemma_collinearorder).
assert (BetS L M K) by (conclude lemma_parallelbetween).
assert (Par G B E F) by (conclude_def PG ).
assert (Col F E K) by (conclude_def Col ).
assert (Col E F K) by (forward_using lemma_collinearorder).
assert (neq F K) by (forward_using lemma_betweennotequal).
assert (neq K F) by (conclude lemma_inequalitysymmetric).
assert (Par G B K F) by (conclude lemma_collinearparallel).
assert (Col F G H) by (forward_using lemma_collinearorder).
assert (BetS F G H) by (conclude lemma_parallelbetween).
assert (BetS H G F) by (conclude axiom_betweennesssymmetry).
assert (PG A B G H) by (conclude lemma_PGrotate).
assert (PG B G H A) by (conclude lemma_PGrotate).
assert (PG G H A B) by (conclude lemma_PGrotate).
assert (PG M K E B) by (conclude lemma_PGrotate).
assert (PG K E B M) by (conclude lemma_PGrotate).
assert (PG E B M K) by (conclude lemma_PGrotate).
assert (EF B E F G L M B A) by (conclude proposition_43).
assert (PG A H G B) by (conclude lemma_PGflip).
assert (PG M B E K) by (conclude lemma_PGflip).
assert (PG A B M L) by (conclude proposition_43B).
assert (Col H G F) by (forward_using lemma_collinearorder).
assert (neq H F) by (forward_using lemma_betweennotequal).
assert (neq L K) by (forward_using lemma_betweennotequal).
assert (neq H G) by (forward_using lemma_betweennotequal).
assert (neq M K) by (forward_using lemma_betweennotequal).
assert (Par H F L K) by (conclude_def PG ).
assert (¬ Meet H F L K)
by (unfold Par in H251;decompose [ex and] H251;auto).
assert (Col G M B) by (forward_using lemma_collinearorder).
assert (BetS G B M) by (conclude lemma_collinearbetween).
assert (CongA A B M G B E) by (conclude proposition_15).
assert (CongA G B E E B G) by (conclude lemma_ABCequalsCBA).
assert (CongA A B M E B G) by (conclude lemma_equalanglestransitive).
assert (CongA A B M J D N) by (conclude lemma_equalanglestransitive).
close.
Qed.
End Euclid.