Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.
Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_26A : 
   forall A B C D E F, 
   Triangle A B C -> Triangle D E F -> CongA A B C D E F -> CongA B C A E F D -> Cong B C E F ->
   Cong A B D E /\ Cong A C D F /\ CongA B A C E D F.
Proof.
(* Goal: forall (A B C D E F : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @Triangle Ax0 D E F) (_ : @CongA Ax0 A B C D E F) (_ : @CongA Ax0 B C A E F D) (_ : @Cong Ax0 B C E F), and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
intros.
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq A B).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq B C).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq A C).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ Lt D E A B).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Cong A B B A) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt D E B A) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists G, (BetS B G A /\ Cong B G D E)) by (conclude_def Lt );destruct Tf as [G];spliter.
(* Goal: False *)
 assert (neq B G) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Cong B G E D) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Out B A G) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out B C C) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Cong G C G C) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (eq G G) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out B G G) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Cong B G B G) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (CongA A B C G B C) by (conclude_def CongA ).
(* Goal: False *)
 assert (CongA G B C A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA G B C D E F) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert ((Cong G C D F /\ CongA B G C E D F /\ CongA B C G E F D)) by (conclude proposition_04).
(* Goal: False *)
 assert (CongA E F D B C A) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA B C G B C A) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (CongA B C A B C G) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (Out C B B) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out C A A) by (conclude lemma_ray4).
(* Goal: False *)
 assert (LtA B C A B C A) by (conclude_def LtA ).
(* Goal: False *)
 assert (~ LtA B C A B C A) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ Lt A B D E).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Cong D E E D) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt A B E D) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists G, (BetS E G D /\ Cong E G A B)) by (conclude_def Lt );destruct Tf as [G];spliter.
(* Goal: False *)
 assert (Cong E G B A) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (neq E D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Out E D G) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (eq F F) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (nCol D E F) by (conclude_def Triangle ).
(* Goal: False *)
 assert (~ eq E F).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
  {
(* Goal: not (@eq Ax0 D E) *)
  intro.
(* Goal: False *)
  assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Out E F F) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Cong G F G F) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (eq G G) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (neq E G) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (Out E G G) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Cong E G E G) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Cong E F E F) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (CongA D E F G E F) by (conclude_def CongA ).
(* Goal: False *)
 assert (CongA G E F D E F) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA D E F A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA G E F A B C) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (Cong E F B C) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert ((Cong G F A C /\ CongA E G F B A C /\ CongA E F G B C A)) by (conclude proposition_04).
(* Goal: False *)
 assert (CongA E F G E F D) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (CongA E F D E F G) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (nCol E F G) by (conclude lemma_equalanglesNC).
(* Goal: False *)
 assert (CongA E F G E F G) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (neq E F) by (forward_using lemma_angledistinct).
(* Goal: False *)
 assert (neq F E) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Out F E E) by (conclude lemma_ray4).
(* Goal: False *)
 assert (neq F D) by (forward_using lemma_angledistinct).
(* Goal: False *)
 assert (Out F D D) by (conclude lemma_ray4).
(* Goal: False *)
 assert (LtA E F D E F D) by (conclude_def LtA ).
(* Goal: False *)
 assert (~ LtA E F D E F D) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq D E).
(* Goal: not (@eq Ax0 D E) *)
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 D E) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
 assert (nCol D E F) by (conclude_def Triangle ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (Cong A B D E) by (conclude lemma_trichotomy1).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (Cong B A E D) by (forward_using lemma_congruenceflip).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert ((Cong A C D F /\ CongA B A C E D F /\ CongA B C A E F D)) by (conclude proposition_04).
(* Goal: and (@Cong Ax0 A B D E) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
close.
Qed.

End Euclid.
