Require Export GeoCoq.Elements.OriginalProofs.lemma_8_2.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_rectanglereverse : 
   forall A B C D, 
   RE A B C D ->
   RE D C B A.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @RE Ax0 A B C D), @RE Ax0 D C B A *)
intros.
(* Goal: @RE Ax0 D C B A *)
assert ((Per D A B /\ Per A B C /\ Per B C D /\ Per C D A /\ CR A C B D)) by (conclude_def RE ).
(* Goal: @RE Ax0 D C B A *)
assert (Per A D C) by (conclude lemma_8_2).
(* Goal: @RE Ax0 D C B A *)
assert (Per D C B) by (conclude lemma_8_2).
(* Goal: @RE Ax0 D C B A *)
assert (Per C B A) by (conclude lemma_8_2).
(* Goal: @RE Ax0 D C B A *)
assert (Per B A D) by (conclude lemma_8_2).
let Tf:=fresh in
assert (Tf:exists M, (BetS A M C /\ BetS B M D)) by (conclude_def CR );destruct Tf as [M];spliter.
(* Goal: @RE Ax0 D C B A *)
assert (BetS C M A) by (conclude axiom_betweennesssymmetry).
(* Goal: @RE Ax0 D C B A *)
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
(* Goal: @RE Ax0 D C B A *)
assert (CR D B C A) by (conclude_def CR ).
(* Goal: @RE Ax0 D C B A *)
assert (RE D C B A) by (conclude_def RE ).
(* Goal: @RE Ax0 D C B A *)
close.
Qed.

End Euclid.


