Require Export GeoCoq.Elements.OriginalProofs.proposition_10.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_09 : 
   forall A B C, 
   nCol B A C ->
   exists X, CongA B A X X A C /\ InAngle B A C X.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @nCol Ax0 B A C), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (~ eq A B).
(* Goal: not (@eq Ax0 A F) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
 {
(* Goal: not (@eq Ax0 A F) *)
 intro.
(* Goal: False *)
 assert (eq B A) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 assert (Col B A C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (~ eq A C).
(* Goal: not (@eq Ax0 A F) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
 {
(* Goal: not (@eq Ax0 A F) *)
 intro.
(* Goal: False *)
 assert (Col B A C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists E, (Out A C E /\ Cong A E A B)) by (conclude lemma_layoff);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (~ eq B E).
(* Goal: not (@eq Ax0 A F) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
 {
(* Goal: not (@eq Ax0 A F) *)
 intro.
(* Goal: False *)
 assert (Col A B E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A C E) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col E A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A E) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq E A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col A B C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col B A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists F, (BetS B F E /\ Cong F B F E)) by (conclude proposition_10);destruct Tf as [F];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (eq F F) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Cong A F A F) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Cong A B A E) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Cong E F B F) by (forward_using lemma_doublereverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Cong B F E F) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (~ Col B A F).
(* Goal: not (@eq Ax0 A F) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
 {
(* Goal: not (@eq Ax0 A F) *)
 intro.
(* Goal: False *)
 assert (Col B F E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col F B E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col F B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B F) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq F B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B E A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A C E) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col E A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A E) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq E A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col A B C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col B A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Out A B B) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (~ eq A F).
(* Goal: not (@eq Ax0 A F) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
 {
(* Goal: not (@eq Ax0 A F) *)
 intro.
(* Goal: False *)
 assert (Col B A F) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (Out A F F) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (CongA B A F C A F) by (conclude_def CongA ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (CongA C A F B A F) by (conclude lemma_equalanglessymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (nCol C A F) by (conclude_def CongA ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (CongA C A F F A C) by (conclude lemma_ABCequalsCBA).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (CongA B A F F A C) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
assert (InAngle B A C F) by (conclude_def InAngle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@CongA Ax0 B A X X A C) (@InAngle Ax0 B A C X)) *)
close.
Qed.

End Euclid.


