Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma proposition_29C : 
   forall B D E G H, 
   Par G B H D -> OS B D G H -> BetS E G H ->
   CongA E G B G H D /\ RT B G H G H D.
Proof.
(* Goal: forall (B D E G H : @Point Ax0) (_ : @Par Ax0 G B H D) (_ : @OS Ax0 B D G H) (_ : @BetS Ax0 E G H), and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
intros.
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (nCol G B H) by (forward_using lemma_parallelNC).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (~ eq G B).
(* Goal: not (@Meet Ax0 A B C D) *)
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
 {
(* Goal: not (@Meet Ax0 A B C D) *)
 intro.
(* Goal: False *)
 assert (Col G B H) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq B G) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists A, (BetS B G A /\ Cong G A B G)) by (conclude lemma_extension);destruct Tf as [A];spliter.
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (BetS A G B) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col A B G) by (conclude_def Col ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col G B A) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par H D G B) by (conclude lemma_parallelsymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par H D A B) by (conclude lemma_collinearparallel).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par H D B A) by (forward_using lemma_parallelflip).
(* Goal: False *)
assert (Col B A G) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq G A) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par H D G A) by (conclude lemma_collinearparallel).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par H D A G) by (forward_using lemma_parallelflip).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par A G H D) by (conclude lemma_parallelsymmetric).
let Tf:=fresh in
assert (Tf:exists a g h d m, (neq A G /\ neq H D /\ Col A G a /\ Col A G g /\ neq a g /\ Col H D h /\ Col H D d /\ neq h d /\ ~ Meet A G H D /\ BetS a m d /\ BetS h m g)) by (conclude_def Par );destruct Tf as [a[g[h[d[m]]]]];spliter.
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq D H) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists C, (BetS D H C /\ Cong H C D H)) by (conclude lemma_extension);destruct Tf as [C];spliter.
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (BetS H G E) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq D C) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq C D) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col A G B) by (conclude_def Col ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col G A B) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col G A a) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (neq G A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col A B a) by (conclude lemma_collinear4).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col G A g) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col A B g) by (conclude lemma_collinear4).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col D H C) by (conclude_def Col ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col H D C) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col D C h) by (conclude lemma_collinear4).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col C D h) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col D d C) by (conclude lemma_collinear4).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col C D d) by (forward_using lemma_collinearorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (~ Meet A B C D).
(* Goal: not (@Meet Ax0 A B C D) *)
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
 {
(* Goal: not (@Meet Ax0 A B C D) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists M, (neq A B /\ neq C D /\ Col A B M /\ Col C D M)) by (conclude_def Meet );destruct Tf as [M];spliter.
(* Goal: False *)
 assert (Col B A G) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B A M) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A G M) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C D H) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D H M) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col H D M) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A G H D) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Par A B C D) by (conclude_def Par ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (BetS C H D) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (BetS E G H) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (eq G G) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (Col G H G) by (conclude_def Col ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (nCol G B H) by (forward_using lemma_parallelNC).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (nCol G H B) by (forward_using lemma_NCorder).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (OS D B G H) by (forward_using lemma_samesidesymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (TS B G H A) by (conclude_def TS ).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (TS D G H A) by (conclude lemma_planeseparation).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert (TS A G H D) by (conclude lemma_oppositesidesymmetric).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
assert ((CongA A G H G H D /\ CongA E G B G H D /\ RT B G H G H D)) by (conclude proposition_29).
(* Goal: and (@CongA Ax0 E G B G H D) (@RT Ax0 B G H G H D) *)
close.
Qed.

End Euclid.


