Require Export GeoCoq.Elements.OriginalProofs.lemma_ray5.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_supplementsymmetric : 
   forall A B C D E, 
   Supp A B C E D ->
   Supp D B E C A.
Proof.
(* Goal: forall (A B C D E : @Point Ax) (_ : @Supp Ax A B C E D), @Supp Ax D B E C A *)
intros.
(* Goal: @Supp Ax D B E C A *)
assert ((Out B C E /\ BetS A B D)) by (conclude_def Supp ).
(* Goal: @Supp Ax D B E C A *)
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @Supp Ax D B E C A *)
assert (Out B E C) by (conclude lemma_ray5).
(* Goal: @Supp Ax D B E C A *)
assert (Supp D B E C A) by (conclude_def Supp ).
(* Goal: @Supp Ax D B E C A *)
close.
Qed.

End Euclid.


