Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_extensionunique.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_rightreverse : 
   forall A B C D, 
   Per A B C -> BetS A B D -> Cong A B B D ->
   Cong A C D C.
Proof.
(* Goal: forall (A B C D : @Point Ax) (_ : @Per Ax A B C) (_ : @BetS Ax A B D) (_ : @Cong Ax A B B D), @Cong Ax A C D C *)
intros.
let Tf:=fresh in
assert (Tf:exists E, (BetS A B E /\ Cong A B E B /\ Cong A C E C /\ neq B C)) by (conclude_def Per );destruct Tf as [E];spliter.
(* Goal: @Cong Ax A C D C *)
assert (Cong B D A B) by (conclude lemma_congruencesymmetric).
(* Goal: @Cong Ax A C D C *)
assert (Cong B D E B) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax A C D C *)
assert (Cong B D B E) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax A C D C *)
assert (eq D E) by (conclude lemma_extensionunique).
(* Goal: @Cong Ax A C D C *)
assert (Cong A C D C) by (conclude cn_equalitysub).
(* Goal: @Cong Ax A C D C *)
close.
Qed.

End Euclid.


