Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_crossimpliesopposite.
Require Export GeoCoq.Elements.OriginalProofs.proposition_34.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma lemma_diagonalsbisect : 
   forall A B C D, 
   PG A B C D ->
   exists X, Midpoint A X C /\ Midpoint B X D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @PG Ax0 A B C D), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
intros.
let Tf:=fresh in
assert (Tf:exists M, (BetS A M C /\ BetS B M D)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert ((Par A B C D /\ Par A D B C)) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CR A C B D) by (conclude_def CR ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Par A B D C) by (forward_using lemma_parallelflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol A B D) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Par B A D C) by (forward_using lemma_parallelflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (BetS C M A) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CR B D A C) by (conclude_def CR ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol A B C) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol B A C) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (TS B A C D) by (forward_using lemma_crossimpliesopposite).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Cong A B D C) by (forward_using proposition_34).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Cong A B C D) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (~ Col M A B).
(* Goal: not (@Col Ax0 M C D) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 {
(* Goal: not (@Col Ax0 M C D) *)
 intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 assert (Col A M C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col M A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A M) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq M A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col A B C) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 assert (nCol A B C) by (forward_using lemma_parallelNC).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Triangle M A B) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (~ Col M C D).
(* Goal: not (@Col Ax0 M C D) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 {
(* Goal: not (@Col Ax0 M C D) *)
 intro.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 assert (Col A M C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col M C A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 assert (neq M C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col C D A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A C D) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
 assert (nCol A C D) by (forward_using lemma_parallelNC).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Triangle M C D) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Par B A C D) by (forward_using lemma_parallelflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A C A C D) by (conclude proposition_29B).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A C B A C) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out A C M) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol A B C) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out A B B) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A C B A M) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A M B A C) by (conclude lemma_equalanglessymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A M A C D) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol A C D) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq C D) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq C A) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out C D D) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out C A M) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A C D A C D) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A C D M C D) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A M M C D) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol A C D) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col A M C) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col A C M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col A C C) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq M C) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol M C D) by (conclude lemma_NChelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA M C D D C M) by (conclude lemma_ABCequalsCBA).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B A M D C M) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Par A B D C) by (forward_using lemma_parallelflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B D B D C) by (conclude proposition_29B).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out B D M) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol B A D) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq B A) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B D A B M) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B M A B D) by (conclude lemma_equalanglessymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B M B D C) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol B D C) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq D C) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq D B) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out D C C) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Out D B M) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B D C B D C) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA B D C M D C) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B M M D C) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol B D C) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col B M D) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col B D M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Col B D D) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (neq M D) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (nCol M D C) by (conclude lemma_NChelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA M D C C D M) by (conclude lemma_ABCequalsCBA).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA A B M C D M) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (CongA M A B M C D) by (conclude lemma_equalanglesflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert ((Cong M A M C /\ Cong M B M D /\ CongA A M B C M D)) by (conclude proposition_26A).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Cong A M M C) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Cong B M M D) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Midpoint A M C) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
assert (Midpoint B M D) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Midpoint Ax0 A X C) (@Midpoint Ax0 B X D)) *)
close.
Qed.

End Euclid.


