Require Export GeoCoq.Elements.OriginalProofs.proposition_47.
Require Export GeoCoq.Elements.OriginalProofs.lemma_squaresequal.
Require Export GeoCoq.Elements.OriginalProofs.lemma_rectanglerotate.
Require Export GeoCoq.Elements.OriginalProofs.lemma_paste5.
Require Export GeoCoq.Elements.OriginalProofs.proposition_48A.
Require Export GeoCoq.Elements.OriginalProofs.proposition_08.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_48 : 
   forall A B C D E F G H K L M, 
   Triangle A B C -> SQ A B F G -> SQ A C K H -> SQ B C E D -> BetS B M C -> BetS E L D -> EF A B F G B M L D -> EF A C K H M C E L -> RE M C E L ->
   Per B A C.
Proof.
(* Goal: forall (A B C D E F G H K L M : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @SQ Ax0 A B F G) (_ : @SQ Ax0 A C K H) (_ : @SQ Ax0 B C E D) (_ : @BetS Ax0 B M C) (_ : @BetS Ax0 E L D) (_ : @EF Ax0 Ax1 Ax2 Ax A B F G B M L D) (_ : @EF Ax0 Ax1 Ax2 Ax A C K H M C E L) (_ : @RE Ax0 M C E L), @Per Ax0 B A C *)
intros.
(* Goal: @Per Ax0 B A C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @Per Ax0 B A C *)
assert (neq A C) by (forward_using lemma_NCdistinct).
(* Goal: @Per Ax0 B A C *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @Per Ax0 B A C *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists R, (BetS B A R /\ Cong A R A B)) by (conclude lemma_extension);destruct Tf as [R];spliter.
(* Goal: @Per Ax0 B A C *)
assert (Col B A R) by (conclude_def Col ).
(* Goal: @Per Ax0 B A C *)
assert (Col A B R) by (forward_using lemma_collinearorder).
(* Goal: @Per Ax0 B A C *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @Per Ax0 B A C *)
assert (Col A B B) by (conclude_def Col ).
(* Goal: @Per Ax0 B A C *)
assert (neq B R) by (forward_using lemma_betweennotequal).
(* Goal: @Per Ax0 B A C *)
assert (neq R B) by (conclude lemma_inequalitysymmetric).
(* Goal: @Per Ax0 B A C *)
assert (nCol R B C) by (conclude lemma_NChelper).
(* Goal: @Per Ax0 B A C *)
assert (nCol B R C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists Q, (Per B A Q /\ TS Q B R C)) by (conclude proposition_11B);destruct Tf as [Q];spliter.
(* Goal: @Per Ax0 B A C *)
assert (nCol B A Q) by (conclude lemma_rightangleNC).
(* Goal: @Per Ax0 B A C *)
assert (neq A Q) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists c, (Out A Q c /\ Cong A c A C)) by (conclude lemma_layoff);destruct Tf as [c];spliter.
(* Goal: @Per Ax0 B A C *)
assert (Per B A c) by (conclude lemma_8_3).
(* Goal: @Per Ax0 B A C *)
assert (nCol B A c) by (conclude lemma_rightangleNC).
(* Goal: @Per Ax0 B A C *)
assert (nCol A B c) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists f g, (SQ A B f g /\ TS g A B c /\ PG A B f g)) by (conclude proposition_46);destruct Tf as [f[g]];spliter.
(* Goal: @Per Ax0 B A C *)
assert (neq A c) by (forward_using lemma_NCdistinct).
(* Goal: @Per Ax0 B A C *)
assert (nCol A c B) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists k h, (SQ A c k h /\ TS h A c B /\ PG A c k h)) by (conclude proposition_46);destruct Tf as [k[h]];spliter.
(* Goal: @Per Ax0 B A C *)
assert (neq B c) by (forward_using lemma_NCdistinct).
(* Goal: @Per Ax0 B A C *)
assert (nCol B c A) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists e d, (SQ B c e d /\ TS d B c A /\ PG B c e d)) by (conclude proposition_46);destruct Tf as [e[d]];spliter.
(* Goal: @Per Ax0 B A C *)
assert (Triangle A B c) by (conclude_def Triangle ).
(* Goal: @Per Ax0 B A C *)
assert (TS g B A c) by (conclude lemma_oppositesideflip).
(* Goal: @Per Ax0 B A C *)
assert (TS h c A B) by (conclude lemma_oppositesideflip).
(* Goal: @Per Ax0 B A C *)
assert (TS d c B A) by (conclude lemma_oppositesideflip).
let Tf:=fresh in
assert (Tf:exists m l, (PG B m l d /\ BetS B m c /\ PG m c e l /\ BetS d l e /\ EF A B f g B m l d /\ EF A c k h m c e l)) by (conclude proposition_47);destruct Tf as [m[l]];spliter.
(* Goal: @Per Ax0 B A C *)
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
(* Goal: @Per Ax0 B A C *)
assert (EF A C K H A c k h) by (conclude lemma_squaresequal).
(* Goal: @Per Ax0 B A C *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @Per Ax0 B A C *)
assert (EF A B F G A B f g) by (conclude lemma_squaresequal).
(* Goal: @Per Ax0 B A C *)
assert (EF A B F G B m l d) by (conclude axiom_EFtransitive).
(* Goal: @Per Ax0 B A C *)
assert (EF B M L D A B F G) by (conclude axiom_EFsymmetric).
(* Goal: @Per Ax0 B A C *)
assert (EF B M L D B m l d) by (conclude axiom_EFtransitive).
(* Goal: @Per Ax0 B A C *)
assert (EF M C E L A C K H) by (conclude axiom_EFsymmetric).
(* Goal: @Per Ax0 B A C *)
assert (EF M C E L A c k h) by (conclude axiom_EFtransitive).
(* Goal: @Per Ax0 B A C *)
assert (EF M C E L m c e l) by (conclude axiom_EFtransitive).
(* Goal: @Per Ax0 B A C *)
assert (BetS e l d) by (conclude axiom_betweennesssymmetry).
(* Goal: @Per Ax0 B A C *)
assert (Per B c e) by (conclude_def SQ ).
(* Goal: @Per Ax0 B A C *)
assert (neq m c) by (forward_using lemma_betweennotequal).
(* Goal: @Per Ax0 B A C *)
assert (Col B m c) by (conclude_def Col ).
(* Goal: @Per Ax0 B A C *)
assert (Col B c m) by (forward_using lemma_collinearorder).
(* Goal: @Per Ax0 B A C *)
assert (Per m c e) by (conclude lemma_collinearright).
(* Goal: @Per Ax0 B A C *)
assert (PG c e l m) by (conclude lemma_PGrotate).
(* Goal: @Per Ax0 B A C *)
assert (RE c e l m) by (conclude lemma_PGrectangle).
(* Goal: @Per Ax0 B A C *)
assert (RE e l m c) by (conclude lemma_rectanglerotate).
(* Goal: @Per Ax0 B A C *)
assert (RE l m c e) by (conclude lemma_rectanglerotate).
(* Goal: @Per Ax0 B A C *)
assert (RE m c e l) by (conclude lemma_rectanglerotate).
(* Goal: @Per Ax0 B A C *)
assert (EF B C E D B c e d) by (conclude lemma_paste5).
(* Goal: @Per Ax0 B A C *)
assert (Cong B C B c) by (conclude proposition_48A).
(* Goal: @Per Ax0 B A C *)
assert (Cong A C A c) by (conclude lemma_congruencesymmetric).
(* Goal: @Per Ax0 B A C *)
assert (Triangle A B c) by (conclude_def Triangle ).
(* Goal: @Per Ax0 B A C *)
assert (CongA B A C B A c) by (apply (proposition_08 A B C A B c);auto).
(* Goal: @Per Ax0 B A C *)
assert (Per B A C) by (conclude lemma_equaltorightisright).
(* Goal: @Per Ax0 B A C *)
close.
Qed.

End Euclid.


