Require Export GeoCoq.Elements.OriginalProofs.lemma_notperp.
Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_11B : 
   forall A B C P, 
   BetS A C B -> nCol A B P ->
   exists X, Per A C X /\ TS X A B P.
Proof.
(* Goal: forall (A B C P : @Point Ax0) (_ : @BetS Ax0 A C B) (_ : @nCol Ax0 A B P), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
intros.
let Tf:=fresh in
assert (Tf:exists M, (nCol A B M /\ OS M P A B /\ ~ Per A C M)) by (conclude lemma_notperp);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq A B) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists Q, Perp_at M Q A B Q) by (conclude proposition_12);destruct Tf as [Q];spliter.
let Tf:=fresh in
assert (Tf:exists E, (Col M Q Q /\ Col A B Q /\ Col A B E /\ Per E Q M)) by (conclude_def Perp_at );destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (~ eq M Q).
(* Goal: not (@eq Ax0 J G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
 {
(* Goal: not (@eq Ax0 J G) *)
 intro.
(* Goal: False *)
 assert (Col A B M) by (conclude cn_equalitysub).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq Q M) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col A B C) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col B A E) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col B A C) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (~ eq C Q).
(* Goal: not (@eq Ax0 J G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
 {
(* Goal: not (@eq Ax0 J G) *)
 intro.
(* Goal: False *)
 assert (Per E C M) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (Col A E C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col E C A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
 assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Per A C M) by (conclude lemma_collinearright).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col C Q E) by (conclude lemma_collinear5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col E Q C) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per C Q M) by (conclude lemma_collinearright).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq Q C) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists G, (BetS Q G C /\ Cong G Q G C)) by (conclude proposition_10);destruct Tf as [G];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (~ eq M G).
(* Goal: not (@eq Ax0 J G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
 {
(* Goal: not (@eq Ax0 J G) *)
 intro.
(* Goal: False *)
 assert (BetS Q M C) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (Col Q M C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B Q C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col Q C M) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq Q C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col C M B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C B M) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C B) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col B M A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B M) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS M G H /\ Cong G H M G)) by (conclude lemma_extension);destruct Tf as [H];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M G G H) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Midpoint M G H) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong Q G G C) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Midpoint Q G C) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col Q G C) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col C Q G) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq Q G) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq G Q) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per G Q M) by (conclude lemma_collinearright).
let Tf:=fresh in
assert (Tf:exists J, (BetS M Q J /\ Cong Q J M Q)) by (conclude lemma_extension);destruct Tf as [J];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per M Q G) by (conclude lemma_8_2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M G J G) by (conclude lemma_rightreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (BetS J Q M) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong J Q M Q) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong J G M G) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per J Q G) by (conclude_def Per ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (~ eq J G).
(* Goal: not (@eq Ax0 J G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
 {
(* Goal: not (@eq Ax0 J G) *)
 intro.
(* Goal: False *)
 assert (Col J Q G) by (conclude_def Col ).
(* Goal: False *)
 assert (nCol J Q G) by (conclude lemma_rightangleNC).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists K, (BetS J G K /\ Cong G K J G)) by (conclude lemma_extension);destruct Tf as [K];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong J G G K) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Midpoint J G K) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M Q H C) by (conclude lemma_pointreflectionisometry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq J Q) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq Q J) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq M J) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong Q J C K) by (conclude lemma_pointreflectionisometry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M J H K) by (conclude lemma_pointreflectionisometry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (BetS H C K) by (conclude lemma_betweennesspreserved).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H G G M) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong G M J G) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H G J G) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong J G G K) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H G G K) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H G K G) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq G C) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H C M Q) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H C Q J) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H C C K) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Cong H C K C) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq G C) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq C G) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per H C G) by (conclude_def Per ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per G C H) by (conclude lemma_8_2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col A B A) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col Q C A) by (conclude lemma_collinear5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col Q C G) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col C A G) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col G C A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Per A C H) by (conclude lemma_collinearright).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col C A B) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col A G B) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (Col A B G) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (OS P M A B) by (forward_using lemma_samesidesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (TS M A B H) by (conclude_def TS ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (TS P A B H) by (conclude lemma_planeseparation).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
assert (TS H A B P) by (conclude lemma_oppositesidesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Per Ax0 A C X) (@TS Ax0 X A B P)) *)
close.
Qed.

End Euclid.
