Require Export GeoCoq.Elements.OriginalProofs.proposition_46.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesideflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_righttogether.
Require Export GeoCoq.Elements.OriginalProofs.lemma_diagonalsbisect.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma lemma_squareparallelogram : 
   forall A B C D, 
   SQ A B C D ->
   PG A B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @SQ Ax0 A B C D), @PG Ax0 A B C D *)
intros.
(* Goal: @PG Ax0 A B C D *)
assert ((Cong A B C D /\ Cong A B B C /\ Cong A B D A /\ Per D A B /\ Per A B C /\ Per B C D /\ Per C D A)) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (nCol D A B) by (conclude lemma_rightangleNC).
(* Goal: @PG Ax0 A B C D *)
assert (neq D A) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists R, (BetS D A R /\ Cong A R D A)) by (conclude lemma_extension);destruct Tf as [R];spliter.
(* Goal: @PG Ax0 A B C D *)
assert (BetS R A D) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 A B C D *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (Col D A R) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col D A A) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (neq R A) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 A B C D *)
assert (nCol R A B) by (conclude lemma_NChelper).
(* Goal: @PG Ax0 A B C D *)
assert (nCol A B R) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists c E, (SQ A B c E /\ TS E A B R /\ PG A B c E)) by (conclude proposition_46);destruct Tf as [c[E]];spliter.
(* Goal: @PG Ax0 A B C D *)
assert ((Cong A B c E /\ Cong A B B c /\ Cong A B E A /\ Per E A B /\ Per A B c /\ Per B c E /\ Per c E A)) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Col R A D) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col D A R) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 A B C D *)
assert (Per R A B) by (conclude lemma_collinearright).
(* Goal: @PG Ax0 A B C D *)
assert (Per B A R) by (conclude lemma_8_2).
(* Goal: @PG Ax0 A B C D *)
assert (TS E B A R) by (conclude lemma_oppositesideflip).
(* Goal: @PG Ax0 A B C D *)
assert (BetS E A R) by (conclude lemma_righttogether).
(* Goal: @PG Ax0 A B C D *)
assert (BetS R A E) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 A B C D *)
assert (Out A D E) by (conclude_def Out ).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A B E A) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Cong E A A B) by (conclude lemma_congruencesymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong E A D A) by (conclude lemma_congruencetransitive).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A E A D) by (forward_using lemma_congruenceflip).
(* Goal: @PG Ax0 A B C D *)
assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 A B C D *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Out A D D) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (eq E D) by (conclude lemma_layoffunique).
(* Goal: @PG Ax0 A B C D *)
assert (PG A B c D) by (conclude cn_equalitysub).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A B C D) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (SQ A B c D) by (conclude cn_equalitysub).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A B c D) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Cong c D A B) by (conclude lemma_congruencesymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong c D C D) by (conclude lemma_congruencetransitive).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A B B C) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A B B c) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Cong B c A B) by (conclude lemma_congruencesymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong B c B C) by (conclude lemma_congruencetransitive).
(* Goal: @PG Ax0 A B C D *)
assert (Cong c B C B) by (forward_using lemma_congruenceflip).
(* Goal: @PG Ax0 A B C D *)
assert (Per B C D) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (Per B c D) by (conclude_def SQ ).
(* Goal: @PG Ax0 A B C D *)
assert (CongA B c D B C D) by (conclude lemma_Euclid4).
(* Goal: @PG Ax0 A B C D *)
assert ((Cong B D B D /\ CongA c B D C B D /\ CongA c D B C D B)) by (conclude proposition_04).
let Tf:=fresh in
assert (Tf:exists m, (Midpoint A m c /\ Midpoint B m D)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];spliter.
(* Goal: @PG Ax0 A B C D *)
assert ((BetS A m c /\ Cong A m m c)) by (conclude_def Midpoint ).
(* Goal: @PG Ax0 A B C D *)
assert ((BetS B m D /\ Cong B m m D)) by (conclude_def Midpoint ).
(* Goal: @PG Ax0 A B C D *)
assert (CongA C D B c D B) by (conclude lemma_equalanglessymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong D m D m) by (conclude cn_congruencereflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Cong D c D C) by (forward_using lemma_congruenceflip).
(* Goal: @PG Ax0 A B C D *)
assert (nCol C D A) by (conclude lemma_rightangleNC).
(* Goal: @PG Ax0 A B C D *)
assert (Per c D A) by (conclude cn_equalitysub).
(* Goal: @PG Ax0 A B C D *)
assert (nCol c D A) by (conclude lemma_rightangleNC).
(* Goal: @PG Ax0 A B C D *)
assert (nCol A c D) by (forward_using lemma_NCorder).
(* Goal: @PG Ax0 A B C D *)
assert (eq c c) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col A c c) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col A m c) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col A c m) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 A B C D *)
assert (neq m c) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 A B C D *)
assert (nCol m c D) by (conclude lemma_NChelper).
(* Goal: @PG Ax0 A B C D *)
assert (nCol c D m) by (forward_using lemma_NCorder).
(* Goal: @PG Ax0 A B C D *)
assert (~ Col C D m).
(* Goal: not (@Col Ax0 C D m) *)
(* Goal: @PG Ax0 A B C D *)
 {
(* Goal: not (@Col Ax0 C D m) *)
 intro.
(* Goal: False *)
 assert (Col B m D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col m D B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col m D C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq m D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col D B C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col B C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (nCol B C D) by (conclude lemma_rightangleNC).
(* Goal: False *)
 contradict.
 }
(* Goal: @PG Ax0 A B C D *)
assert (CongA c D B C D B) by (conclude lemma_equalanglessymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (BetS D m B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 A B C D *)
assert (neq D B) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 A B C D *)
assert (Out D B m) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (neq D C) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (Out D C C) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (CongA c D B C D m) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 A B C D *)
assert (CongA C D m c D B) by (conclude lemma_equalanglessymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (eq c c) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (neq D c) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (Out D c c) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (CongA C D m c D m) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 A B C D *)
assert (CongA c D m C D m) by (conclude lemma_equalanglessymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong c m C m) by (conclude proposition_04).
(* Goal: @PG Ax0 A B C D *)
assert (Cong m c m C) by (forward_using lemma_congruenceflip).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A m A m) by (conclude cn_congruencereflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Cong D A D A) by (conclude cn_congruencereflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Per c D A) by (conclude cn_equalitysub).
(* Goal: @PG Ax0 A B C D *)
assert (Per A D c) by (conclude lemma_8_2).
(* Goal: @PG Ax0 A B C D *)
assert (Per A D C) by (conclude lemma_8_2).
(* Goal: @PG Ax0 A B C D *)
assert (CongA A D C A D c) by (conclude lemma_Euclid4).
(* Goal: @PG Ax0 A B C D *)
assert (Cong D C D c) by (conclude lemma_congruencesymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A C A c) by (conclude proposition_04).
(* Goal: @PG Ax0 A B C D *)
assert (Cong A c A C) by (conclude lemma_congruencesymmetric).
(* Goal: @PG Ax0 A B C D *)
assert (BetS A m C) by (conclude lemma_betweennesspreserved).
(* Goal: @PG Ax0 A B C D *)
assert (neq A m) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 A B C D *)
assert (Out A m c) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (Out A m C) by (conclude lemma_ray4).
(* Goal: @PG Ax0 A B C D *)
assert (eq c C) by (conclude lemma_layoffunique).
(* Goal: @PG Ax0 A B C D *)
assert (PG A B C D) by (conclude cn_equalitysub).
(* Goal: @PG Ax0 A B C D *)
close.
Qed.

End Euclid.


