Require Export GeoCoq.Elements.OriginalProofs.proposition_31.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_31short : 
   forall A B C D, 
   BetS B D C -> nCol B C A ->
   exists X Y Z, BetS X A Y /\ CongA X A D A D C /\ Par X Y B C /\ BetS X Z C /\ BetS A Z D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @BetS Ax0 B D C) (_ : @nCol Ax0 B C A), @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@BetS Ax0 X A Y) (and (@CongA Ax0 X A D A D C) (and (@Par Ax0 X Y B C) (and (@BetS Ax0 X Z C) (@BetS Ax0 A Z D))))))) *)
intros.
let Tf:=fresh in
assert (Tf:exists E F S, (BetS E A F /\ CongA F A D A D B /\ CongA F A D B D A /\ CongA D A F B D A /\ CongA E A D A D C /\ CongA E A D C D A /\ CongA D A E C D A /\ Par E F B C /\ Cong E A D C /\ Cong A F B D /\ Cong A S S D /\ Cong E S S C /\ Cong B S S F /\ BetS E S C /\ BetS B S F /\ BetS A S D)) by (conclude proposition_31);destruct Tf as [E[F[S]]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@BetS Ax0 X A Y) (and (@CongA Ax0 X A D A D C) (and (@Par Ax0 X Y B C) (and (@BetS Ax0 X Z C) (@BetS Ax0 A Z D))))))) *)
close.
Qed.

End Euclid.


