Library GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram

Require Export GeoCoq.Elements.OriginalProofs.proposition_33.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_Playfair.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma lemma_triangletoparallelogram :
    A C D E F,
   Par D C E F Col E F A
    X, PG A X C D Col E F X.
Proof.
intros.
assert (nCol D C E) by (forward_using lemma_parallelNC).
assert (neq D C) by (forward_using lemma_NCdistinct).
assert (neq C D) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf: B, (BetS C D B Cong D B C D)) by (conclude postulate_extension);destruct Tf as [B];spliter.
assert (BetS B D C) by (conclude axiom_betweennesssymmetry).
assert (nCol C E F) by (forward_using lemma_parallelNC).
assert (neq E F) by (forward_using lemma_NCdistinct).
assert (¬ Col B C A).
 {
 intro.
 assert (Col C D B) by (conclude_def Col ).
 assert (Col B C D) by (forward_using lemma_collinearorder).
 assert (neq B C) by (forward_using lemma_betweennotequal).
 assert (Col C A D) by (conclude lemma_collinear4).
 assert (Col D C A) by (forward_using lemma_collinearorder).
 assert (neq C D) by (forward_using lemma_betweennotequal).
 assert (Meet D C E F) by (conclude_def Meet ).
 assert (¬ Meet D C E F) by (conclude_def Par ).
 contradict.
 }
let Tf:=fresh in
assert (Tf: c b M, (BetS c A b CongA b A D A D B CongA b A D B D A CongA D A b B D A CongA c A D A D C CongA c A D C D A CongA D A c C D A Par c b B C Cong c A D C Cong A b B D Cong A M M D Cong c M M C Cong B M M b BetS c M C BetS B M b BetS A M D)) by (conclude proposition_31);destruct Tf as [c[b[M]]];spliter.
assert (BetS b M B) by (conclude axiom_betweennesssymmetry).
assert (nCol b B C) by (forward_using lemma_parallelNC).
let Tf:=fresh in
assert (Tf: R, (BetS b R D BetS C R M)) by (conclude postulate_Pasch_inner);destruct Tf as [R];spliter.
assert (BetS C M c) by (conclude axiom_betweennesssymmetry).
assert (BetS C R c) by (conclude lemma_3_6b).
assert (BetS b A c) by (conclude axiom_betweennesssymmetry).
assert (nCol c b C) by (forward_using lemma_parallelNC).
assert (nCol b c C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf: Q, (BetS b Q R BetS C Q A)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.
assert (BetS b Q D) by (conclude lemma_3_6b).
assert (Col C D B) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col B C C) by (conclude_def Col ).
assert (Par c b D C) by (conclude lemma_collinearparallel).
assert (Par D C c b) by (conclude lemma_parallelsymmetric).
assert (Col c A b) by (conclude_def Col ).
assert (Col c b A) by (forward_using lemma_collinearorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col C b b) by (conclude_def Col ).
assert (neq A b) by (forward_using lemma_betweennotequal).
assert (Par D C A b) by (conclude lemma_collinearparallel).
assert (Par A b D C) by (conclude lemma_parallelsymmetric).
assert (Par b A C D) by (forward_using lemma_parallelflip).
assert (Cong B D D B) by (conclude cn_equalityreverse).
assert (Cong A b D B) by (conclude lemma_congruencetransitive).
assert (Cong A b C D) by (conclude lemma_congruencetransitive).
assert (Cong b A C D) by (forward_using lemma_congruenceflip).
assert (BetS A Q C) by (conclude axiom_betweennesssymmetry).
assert ((Par b C A D Cong b C A D)) by (conclude proposition_33).
assert (Par A b C D) by (forward_using lemma_parallelflip).
assert (Par A D b C) by (conclude lemma_parallelsymmetric).
assert (PG A b C D) by (conclude_def PG ).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col E F E) by (conclude_def Col ).
assert (Col E F F) by (conclude_def Col ).
assert (Col E F b).
by cases on (eq A F neq A F).
{
 assert (neq F E) by (conclude lemma_inequalitysymmetric).
 assert (neq A E) by (conclude cn_equalitysub).
 assert (Par D C A E) by (conclude lemma_collinearparallel2).
 assert (Col A b E) by (conclude lemma_Playfair).
 assert (Col F b E) by (conclude cn_equalitysub).
 assert (Col E F b) by (forward_using lemma_collinearorder).
 close.
 }
{
 assert (Par D C A F) by (conclude lemma_collinearparallel).
 assert (Col A b F) by (conclude lemma_Playfair).
 assert (Col A F b) by (forward_using lemma_collinearorder).
 assert (Col A F E) by (forward_using lemma_collinearorder).
 assert (Col F b E) by (conclude lemma_collinear4).
 assert (Col E F b) by (forward_using lemma_collinearorder).
 close.
 }

close.
Qed.

End Euclid.