Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.proposition_28A.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelsymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_28D : 
   forall B D E G H, 
   BetS E G H -> CongA E G B G H D -> OS B D G H ->
   Par G B H D.
Proof.
(* Goal: forall (B D E G H : @Point Ax0) (_ : @BetS Ax0 E G H) (_ : @CongA Ax0 E G B G H D) (_ : @OS Ax0 B D G H), @Par Ax0 G B H D *)
intros.
(* Goal: @Par Ax0 G B H D *)
assert (nCol G H B) by (conclude_def OS ).
(* Goal: @Par Ax0 G B H D *)
assert (nCol G H D) by (conclude_def OS ).
(* Goal: @Par Ax0 G B H D *)
assert (neq H D) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 G B H D *)
assert (neq D H) by (conclude lemma_inequalitysymmetric).
(* Goal: @Par Ax0 G B H D *)
assert (neq G B) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 G B 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 G B)) by (conclude lemma_extension);destruct Tf as [A];spliter.
(* Goal: @Par Ax0 G B H D *)
assert (BetS A G B) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists C, (BetS D H C /\ Cong H C H D)) by (conclude lemma_extension);destruct Tf as [C];spliter.
(* Goal: @Par Ax0 G B H D *)
assert (BetS C H D) by (conclude axiom_betweennesssymmetry).
(* Goal: @Par Ax0 G B H D *)
assert (Par A B C D) by (conclude proposition_28A).
(* Goal: @Par Ax0 G B H D *)
assert (Col D H C) by (conclude_def Col ).
(* Goal: @Par Ax0 G B H D *)
assert (Col C D H) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 G B H D *)
assert (neq H D) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 G B H D *)
assert (Par A B H D) by (conclude lemma_collinearparallel).
(* Goal: @Par Ax0 G B H D *)
assert (Par H D A B) by (conclude lemma_parallelsymmetric).
(* Goal: @Par Ax0 G B H D *)
assert (Col B G A) by (conclude_def Col ).
(* Goal: @Par Ax0 G B H D *)
assert (Col A B G) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 G B H D *)
assert (Par H D G B) by (conclude lemma_collinearparallel).
(* Goal: @Par Ax0 G B H D *)
assert (Par G B H D) by (conclude lemma_parallelsymmetric).
(* Goal: @Par Ax0 G B H D *)
close.
Qed.

End Euclid.


