Require Export GeoCoq.Elements.OriginalProofs.lemma_8_7.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_rectangleparallelogram : 
   forall A B C D, 
   RE A B C D ->
   PG A B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @RE Ax0 A B C D), @PG Ax0 A B C D *)
intros.
(* Goal: @PG Ax0 A B C D *)
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: @PG Ax0 A B C D *)
assert (nCol D A B) by (conclude lemma_rightangleNC).
(* Goal: @PG Ax0 A B C D *)
assert (nCol A B C) by (conclude lemma_rightangleNC).
(* Goal: @PG Ax0 A B C D *)
assert (nCol C D A) by (conclude lemma_rightangleNC).
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: @PG Ax0 A B C D *)
assert (~ Meet A B C D).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
 {
(* Goal: not (@eq Ax0 B P) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists P, (neq A B /\ neq C D /\ Col A B P /\ Col C D P)) by (conclude_def Meet );destruct Tf as [P];spliter.
(* Goal: False *)
 assert (~ eq A P).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax0 B P) *)
  intro.
(* Goal: False *)
  assert (Col C D A) by (conclude cn_equalitysub).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ eq D P).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax0 B P) *)
  intro.
(* Goal: False *)
  assert (Col A B D) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col D A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Per B A D) by (conclude lemma_8_2).
(* Goal: False *)
 assert (Col B A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq P A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Per P A D) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (neq P D) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Per P D A) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (Per A D P) by (conclude lemma_8_2).
(* Goal: False *)
 assert (~ Per P A D) by (conclude lemma_8_7).
(* Goal: False *)
 contradict.
 }
(* Goal: @PG Ax0 A B C D *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (neq C D) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (neq D C) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col A B A) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col A B B) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col C D C) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col C D D) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 A B C D *)
assert (Par A B C D) by (conclude_def Par ).
(* Goal: @PG Ax0 A B C D *)
assert (~ Meet A D B C).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
 {
(* Goal: not (@eq Ax0 B P) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists P, (neq A D /\ neq B C /\ Col A D P /\ Col B C P)) by (conclude_def Meet );destruct Tf as [P];spliter.
(* Goal: False *)
 assert (~ eq A P).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax0 B P) *)
  intro.
(* Goal: False *)
  assert (Col B C A) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ eq B P).
(* Goal: not (@eq Ax0 B P) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax0 B P) *)
  intro.
(* Goal: False *)
  assert (Col A D B) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col D A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (neq P A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col D A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Per P A B) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (Per C B A) by (conclude lemma_8_2).
(* Goal: False *)
 assert (Col C B P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq P B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Per P B A) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (Per B A P) by (conclude lemma_8_2).
(* Goal: False *)
 assert (~ Per P B A) by (conclude lemma_8_7).
(* Goal: False *)
 contradict.
 }
(* Goal: @PG Ax0 A B C D *)
assert (neq A D) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @PG Ax0 A B C D *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 A B C D *)
assert (Col A D A) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col A D D) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col B C B) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Col B C C) by (conclude_def Col ).
(* Goal: @PG Ax0 A B C D *)
assert (Par A D B C) by (conclude_def Par ).
(* Goal: @PG Ax0 A B C D *)
assert (PG A B C D) by (conclude_def PG ).
(* Goal: @PG Ax0 A B C D *)
close.
Qed.

End Euclid.


