Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_27.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_28A : 
   forall A B C D E G H, 
   BetS A G B -> BetS C H D -> BetS E G H -> CongA E G B G H D -> OS B D G H ->
   Par A B C D.
Proof.
(* Goal: forall (A B C D E G H : @Point Ax0) (_ : @BetS Ax0 A G B) (_ : @BetS Ax0 C H D) (_ : @BetS Ax0 E G H) (_ : @CongA Ax0 E G B G H D) (_ : @OS Ax0 B D G H), @Par Ax0 A B C D *)
intros.
(* Goal: @Par Ax0 A B C D *)
assert (OS D B G H) by (forward_using lemma_samesidesymmetric).
(* Goal: @Par Ax0 A B C D *)
assert (nCol E G B) by (conclude_def CongA ).
(* Goal: @Par Ax0 A B C D *)
assert (eq G G) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A B C D *)
assert (Col G H G) by (conclude_def Col ).
(* Goal: @Par Ax0 A B C D *)
assert (~ Col G H A).
(* Goal: not (@Col Ax0 G H A) *)
(* Goal: @Par Ax0 A B C D *)
 {
(* Goal: not (@Col Ax0 G H A) *)
 intro.
(* Goal: False *)
 assert (Col H G A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E G H) by (conclude_def Col ).
(* Goal: False *)
 assert (Col H G E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq G H) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq H G) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col G A E) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A G E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A G B) by (conclude_def Col ).
(* Goal: False *)
 assert (neq A G) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col G E B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col E G B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @Par Ax0 A B C D *)
assert (TS A G H B) by (conclude_def TS ).
(* Goal: @Par Ax0 A B C D *)
assert (TS B G H A) by (conclude lemma_oppositesidesymmetric).
(* Goal: @Par Ax0 A B C D *)
assert (BetS B G A) by (conclude axiom_betweennesssymmetry).
(* Goal: @Par Ax0 A B C D *)
assert (CongA E G B A G H) by (conclude proposition_15a).
(* Goal: @Par Ax0 A B C D *)
assert (CongA A G H E G B) by (conclude lemma_equalanglessymmetric).
(* Goal: @Par Ax0 A B C D *)
assert (CongA A G H G H D) by (conclude lemma_equalanglestransitive).
(* Goal: @Par Ax0 A B C D *)
assert (TS D G H A) by (conclude lemma_planeseparation).
(* Goal: @Par Ax0 A B C D *)
assert (TS A G H D) by (conclude lemma_oppositesidesymmetric).
(* Goal: @Par Ax0 A B C D *)
assert (Par A B C D) by (conclude proposition_27).
(* Goal: @Par Ax0 A B C D *)
close.
Qed.

End Euclid.


