Require Export GeoCoq.Elements.OriginalProofs.proposition_01.
Require Export GeoCoq.Elements.OriginalProofs.proposition_03.
Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.
Require Export GeoCoq.Elements.OriginalProofs.lemma_twolines.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_10 : 
   forall A B, 
   neq A B ->
   exists X, BetS A X B /\ Cong X A X B.
Proof.
(* Goal: forall (A B : @Point Ax0) (_ : @neq Ax0 A B), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
intros.
let Tf:=fresh in
assert (Tf:exists C, (equilateral A B C /\ Triangle A B C)) by (conclude proposition_01);destruct Tf as [C];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert ((Cong A B B C /\ Cong B C C A)) by (conclude_def equilateral ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A C C B) by (forward_using lemma_doublereverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A C B C) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ eq C B).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col A C B) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists D, (BetS C B D /\ Cong B D A B)) by (conclude lemma_extension);destruct Tf as [D];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ eq C A).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col B C A) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists E, (BetS C A E /\ Cong A E A B)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS D B C) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS E A C) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ Col D C E).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col C A E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col C B D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col E C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C D A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col D C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C B A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists F, (BetS D F A /\ BetS E F B)) by (conclude postulate_Pasch_inner);destruct Tf as [F];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS B F E) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS A F D) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
assert (neq D C) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ Col A D C).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col C B D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C A B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists M, (BetS A M B /\ BetS C M F)) by (conclude postulate_Pasch_inner);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong C A C B) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A B A E) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong B D A E) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A E B D) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A B B A) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong C B C A) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong B E A D) by (conclude axiom_5_line).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong B F B F) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Lt B F B E) by (conclude_def Lt ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A D B E) by (conclude lemma_congruencesymmetric).
let Tf:=fresh in
assert (Tf:exists G, (BetS A G D /\ Cong A G B F)) by (conclude proposition_03);destruct Tf as [G];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong G D F E) by (conclude lemma_differenceofparts).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong E F D G) by (forward_using lemma_doublereverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong F B G A) by (forward_using lemma_doublereverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong E A D B) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong B A A B) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS D G A) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong F A G B) by (conclude lemma_interior5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A F B G) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong E D D E) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong F D G E) by (conclude lemma_interior5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS B G E) by (conclude lemma_betweennesspreserved).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (BetS E G B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ Col A D E).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col C A E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A E D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col E D C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col E C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C D A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C B D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C A B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ Col A D B).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col D B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C B D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cut A D E B G) by (conclude_def Cut ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cut A D E B F) by (conclude_def Cut ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (~ Col D E B).
(* Goal: not (@Col Ax0 D E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
 {
(* Goal: not (@Col Ax0 D E B) *)
 intro.
(* Goal: False *)
 assert (Col C B D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D B E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B C E) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C A E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col E C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C A B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (eq G F) by (conclude lemma_twolines).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong A F B F) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong F A F B) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong C M C M) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong M F M F) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
assert (Cong M A M B) by (conclude lemma_interior5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 A X B) (@Cong Ax0 X A X B)) *)
close.
Qed.

End Euclid.


