# Library GeoCoq.Elements.OriginalProofs.lemma_squareparallelogram

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 :

∀ A B C D,

SQ A B C D →

PG A B C D.

Proof.

intros.

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 ).

assert (nCol D A B) by (conclude lemma_rightangleNC).

assert (neq D A) by (forward_using lemma_NCdistinct).

assert (neq A D) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ R, (BetS D A R ∧ Cong A R D A)) by (conclude postulate_extension);destruct Tf as [R];spliter.

assert (BetS R A D) by (conclude axiom_betweennesssymmetry).

assert (neq A B) by (forward_using lemma_NCdistinct).

assert (Col D A R) by (conclude_def Col ).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col D A A) by (conclude_def Col ).

assert (neq R A) by (forward_using lemma_betweennotequal).

assert (nCol R A B) by (conclude lemma_NChelper).

assert (nCol A B R) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ 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.

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 ).

assert (Col R A D) by (conclude_def Col ).

assert (Col D A R) by (forward_using lemma_collinearorder).

assert (Per R A B) by (conclude lemma_collinearright).

assert (Per B A R) by (conclude lemma_8_2).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col B A A) by (conclude_def Col ).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (TS E B A R) by (conclude lemma_oppositesideflip).

assert (BetS E A R) by (conclude lemma_righttogether).

assert (BetS R A E) by (conclude axiom_betweennesssymmetry).

assert (Out A D E) by (conclude_def Out ).

assert (Cong A B E A) by (conclude_def SQ ).

assert (Cong E A A B) by (conclude lemma_congruencesymmetric).

assert (Cong E A D A) by (conclude lemma_congruencetransitive).

assert (Cong A E A D) by (forward_using lemma_congruenceflip).

assert (neq A D) by (forward_using lemma_betweennotequal).

assert (eq D D) by (conclude cn_equalityreflexive).

assert (Out A D D) by (conclude lemma_ray4).

assert (eq E D) by (conclude lemma_layoffunique).

assert (PG A B c D) by (conclude cn_equalitysub).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (neq C B) by (forward_using lemma_NCdistinct).

assert (Cong A B C D) by (conclude_def SQ ).

assert (SQ A B c D) by (conclude cn_equalitysub).

assert (Cong A B c D) by (conclude_def SQ ).

assert (Cong c D A B) by (conclude lemma_congruencesymmetric).

assert (Cong c D C D) by (conclude lemma_congruencetransitive).

assert (Cong A B B C) by (conclude_def SQ ).

assert (Cong A B B c) by (conclude_def SQ ).

assert (Cong B c A B) by (conclude lemma_congruencesymmetric).

assert (Cong B c B C) by (conclude lemma_congruencetransitive).

assert (Cong c B C B) by (forward_using lemma_congruenceflip).

assert (Per B C D) by (conclude_def SQ ).

assert (Per B c D) by (conclude_def SQ ).

assert (CongA B c D B C D) by (conclude lemma_Euclid4).

assert (nCol B c D) by (conclude lemma_rightangleNC).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (Triangle B C D) by (conclude_def Triangle ).

assert (Triangle B c D) by (conclude_def Triangle ).

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:∃ m, (Midpoint A m c ∧ Midpoint B m D)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];spliter.

assert ((BetS A m c ∧ Cong A m m c)) by (conclude_def Midpoint ).

assert ((BetS B m D ∧ Cong B m m D)) by (conclude_def Midpoint ).

assert (Per D c B) by (conclude lemma_8_2).

assert (Per D C B) by (conclude lemma_8_2).

assert (CongA C D B c D B) by (conclude lemma_equalanglessymmetric).

assert (Cong D m D m) by (conclude cn_congruencereflexive).

assert (Cong D c D C) by (forward_using lemma_congruenceflip).

assert (nCol C D A) by (conclude lemma_rightangleNC).

assert (Per c D A) by (conclude cn_equalitysub).

assert (nCol c D A) by (conclude lemma_rightangleNC).

assert (nCol A c D) by (forward_using lemma_NCorder).

assert (eq c c) by (conclude cn_equalityreflexive).

assert (Col A c c) by (conclude_def Col ).

assert (eq m m) by (conclude cn_equalityreflexive).

assert (Col A m c) by (conclude_def Col ).

assert (Col A c m) by (forward_using lemma_collinearorder).

assert (neq m c) by (forward_using lemma_betweennotequal).

assert (nCol m c D) by (conclude lemma_NChelper).

assert (nCol c D m) by (forward_using lemma_NCorder).

assert (Triangle c D m) by (conclude_def Triangle ).

assert (¬ Col C D m).

{

intro.

assert (Col B m D) by (conclude_def Col ).

assert (Col m D B) by (forward_using lemma_collinearorder).

assert (Col m D C) by (forward_using lemma_collinearorder).

assert (neq m D) by (forward_using lemma_betweennotequal).

assert (Col D B C) by (conclude lemma_collinear4).

assert (Col B C D) by (forward_using lemma_collinearorder).

assert (nCol B C D) by (conclude lemma_rightangleNC).

contradict.

}

assert (Triangle C D m) by (conclude_def Triangle ).

assert (CongA c D B C D B) by (conclude lemma_equalanglessymmetric).

assert (BetS D m B) by (conclude axiom_betweennesssymmetry).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (Out D B m) by (conclude lemma_ray4).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (neq D C) by (forward_using lemma_NCdistinct).

assert (Out D C C) by (conclude lemma_ray4).

assert (CongA c D B C D m) by (conclude lemma_equalangleshelper).

assert (CongA C D m c D B) by (conclude lemma_equalanglessymmetric).

assert (eq c c) by (conclude cn_equalityreflexive).

assert (neq D c) by (forward_using lemma_NCdistinct).

assert (Out D c c) by (conclude lemma_ray4).

assert (CongA C D m c D m) by (conclude lemma_equalangleshelper).

assert (CongA c D m C D m) by (conclude lemma_equalanglessymmetric).

assert (Cong c m C m) by (conclude proposition_04).

assert (Cong m c m C) by (forward_using lemma_congruenceflip).

assert (Cong A m A m) by (conclude cn_congruencereflexive).

assert (Cong D A D A) by (conclude cn_congruencereflexive).

assert (Per c D A) by (conclude cn_equalitysub).

assert (Per A D c) by (conclude lemma_8_2).

assert (Per A D C) by (conclude lemma_8_2).

assert (CongA A D C A D c) by (conclude lemma_Euclid4).

assert (nCol A D C) by (conclude lemma_rightangleNC).

assert (nCol A D c) by (conclude lemma_rightangleNC).

assert (Triangle A D C) by (conclude_def Triangle ).

assert (Triangle A D c) by (conclude_def Triangle ).

assert (Cong D C D c) by (conclude lemma_congruencesymmetric).

assert (Cong A C A c) by (conclude proposition_04).

assert (Cong A c A C) by (conclude lemma_congruencesymmetric).

assert (BetS A m C) by (conclude lemma_betweennesspreserved).

assert (neq A m) by (forward_using lemma_betweennotequal).

assert (Out A m c) by (conclude lemma_ray4).

assert (Out A m C) by (conclude lemma_ray4).

assert (eq c C) by (conclude lemma_layoffunique).

assert (PG A B C D) by (conclude cn_equalitysub).

close.

Qed.

End Euclid.

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 :

∀ A B C D,

SQ A B C D →

PG A B C D.

Proof.

intros.

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 ).

assert (nCol D A B) by (conclude lemma_rightangleNC).

assert (neq D A) by (forward_using lemma_NCdistinct).

assert (neq A D) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ R, (BetS D A R ∧ Cong A R D A)) by (conclude postulate_extension);destruct Tf as [R];spliter.

assert (BetS R A D) by (conclude axiom_betweennesssymmetry).

assert (neq A B) by (forward_using lemma_NCdistinct).

assert (Col D A R) by (conclude_def Col ).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col D A A) by (conclude_def Col ).

assert (neq R A) by (forward_using lemma_betweennotequal).

assert (nCol R A B) by (conclude lemma_NChelper).

assert (nCol A B R) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ 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.

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 ).

assert (Col R A D) by (conclude_def Col ).

assert (Col D A R) by (forward_using lemma_collinearorder).

assert (Per R A B) by (conclude lemma_collinearright).

assert (Per B A R) by (conclude lemma_8_2).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col B A A) by (conclude_def Col ).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (TS E B A R) by (conclude lemma_oppositesideflip).

assert (BetS E A R) by (conclude lemma_righttogether).

assert (BetS R A E) by (conclude axiom_betweennesssymmetry).

assert (Out A D E) by (conclude_def Out ).

assert (Cong A B E A) by (conclude_def SQ ).

assert (Cong E A A B) by (conclude lemma_congruencesymmetric).

assert (Cong E A D A) by (conclude lemma_congruencetransitive).

assert (Cong A E A D) by (forward_using lemma_congruenceflip).

assert (neq A D) by (forward_using lemma_betweennotequal).

assert (eq D D) by (conclude cn_equalityreflexive).

assert (Out A D D) by (conclude lemma_ray4).

assert (eq E D) by (conclude lemma_layoffunique).

assert (PG A B c D) by (conclude cn_equalitysub).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (neq C B) by (forward_using lemma_NCdistinct).

assert (Cong A B C D) by (conclude_def SQ ).

assert (SQ A B c D) by (conclude cn_equalitysub).

assert (Cong A B c D) by (conclude_def SQ ).

assert (Cong c D A B) by (conclude lemma_congruencesymmetric).

assert (Cong c D C D) by (conclude lemma_congruencetransitive).

assert (Cong A B B C) by (conclude_def SQ ).

assert (Cong A B B c) by (conclude_def SQ ).

assert (Cong B c A B) by (conclude lemma_congruencesymmetric).

assert (Cong B c B C) by (conclude lemma_congruencetransitive).

assert (Cong c B C B) by (forward_using lemma_congruenceflip).

assert (Per B C D) by (conclude_def SQ ).

assert (Per B c D) by (conclude_def SQ ).

assert (CongA B c D B C D) by (conclude lemma_Euclid4).

assert (nCol B c D) by (conclude lemma_rightangleNC).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (Triangle B C D) by (conclude_def Triangle ).

assert (Triangle B c D) by (conclude_def Triangle ).

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:∃ m, (Midpoint A m c ∧ Midpoint B m D)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];spliter.

assert ((BetS A m c ∧ Cong A m m c)) by (conclude_def Midpoint ).

assert ((BetS B m D ∧ Cong B m m D)) by (conclude_def Midpoint ).

assert (Per D c B) by (conclude lemma_8_2).

assert (Per D C B) by (conclude lemma_8_2).

assert (CongA C D B c D B) by (conclude lemma_equalanglessymmetric).

assert (Cong D m D m) by (conclude cn_congruencereflexive).

assert (Cong D c D C) by (forward_using lemma_congruenceflip).

assert (nCol C D A) by (conclude lemma_rightangleNC).

assert (Per c D A) by (conclude cn_equalitysub).

assert (nCol c D A) by (conclude lemma_rightangleNC).

assert (nCol A c D) by (forward_using lemma_NCorder).

assert (eq c c) by (conclude cn_equalityreflexive).

assert (Col A c c) by (conclude_def Col ).

assert (eq m m) by (conclude cn_equalityreflexive).

assert (Col A m c) by (conclude_def Col ).

assert (Col A c m) by (forward_using lemma_collinearorder).

assert (neq m c) by (forward_using lemma_betweennotequal).

assert (nCol m c D) by (conclude lemma_NChelper).

assert (nCol c D m) by (forward_using lemma_NCorder).

assert (Triangle c D m) by (conclude_def Triangle ).

assert (¬ Col C D m).

{

intro.

assert (Col B m D) by (conclude_def Col ).

assert (Col m D B) by (forward_using lemma_collinearorder).

assert (Col m D C) by (forward_using lemma_collinearorder).

assert (neq m D) by (forward_using lemma_betweennotequal).

assert (Col D B C) by (conclude lemma_collinear4).

assert (Col B C D) by (forward_using lemma_collinearorder).

assert (nCol B C D) by (conclude lemma_rightangleNC).

contradict.

}

assert (Triangle C D m) by (conclude_def Triangle ).

assert (CongA c D B C D B) by (conclude lemma_equalanglessymmetric).

assert (BetS D m B) by (conclude axiom_betweennesssymmetry).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (Out D B m) by (conclude lemma_ray4).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (neq D C) by (forward_using lemma_NCdistinct).

assert (Out D C C) by (conclude lemma_ray4).

assert (CongA c D B C D m) by (conclude lemma_equalangleshelper).

assert (CongA C D m c D B) by (conclude lemma_equalanglessymmetric).

assert (eq c c) by (conclude cn_equalityreflexive).

assert (neq D c) by (forward_using lemma_NCdistinct).

assert (Out D c c) by (conclude lemma_ray4).

assert (CongA C D m c D m) by (conclude lemma_equalangleshelper).

assert (CongA c D m C D m) by (conclude lemma_equalanglessymmetric).

assert (Cong c m C m) by (conclude proposition_04).

assert (Cong m c m C) by (forward_using lemma_congruenceflip).

assert (Cong A m A m) by (conclude cn_congruencereflexive).

assert (Cong D A D A) by (conclude cn_congruencereflexive).

assert (Per c D A) by (conclude cn_equalitysub).

assert (Per A D c) by (conclude lemma_8_2).

assert (Per A D C) by (conclude lemma_8_2).

assert (CongA A D C A D c) by (conclude lemma_Euclid4).

assert (nCol A D C) by (conclude lemma_rightangleNC).

assert (nCol A D c) by (conclude lemma_rightangleNC).

assert (Triangle A D C) by (conclude_def Triangle ).

assert (Triangle A D c) by (conclude_def Triangle ).

assert (Cong D C D c) by (conclude lemma_congruencesymmetric).

assert (Cong A C A c) by (conclude proposition_04).

assert (Cong A c A C) by (conclude lemma_congruencesymmetric).

assert (BetS A m C) by (conclude lemma_betweennesspreserved).

assert (neq A m) by (forward_using lemma_betweennotequal).

assert (Out A m c) by (conclude lemma_ray4).

assert (Out A m C) by (conclude lemma_ray4).

assert (eq c C) by (conclude lemma_layoffunique).

assert (PG A B C D) by (conclude cn_equalitysub).

close.

Qed.

End Euclid.