Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_06a : 
   forall A B C, 
   Triangle A B C -> CongA A B C A C B ->
   ~ Lt A C A B.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @CongA Ax0 A B C A C B), not (@Lt Ax0 A C A B) *)
intros.
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq A B) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq A C) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq B C) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax0 A C A B) *)
assert (~ Lt A C A B).
(* Goal: not (@Col Ax0 B C D) *)
(* Goal: False *)
 {
(* Goal: not (@Col Ax0 B C D) *)
 intro.
(* Goal: False *)
 assert (Cong B A A B) by (conclude cn_equalityreverse).
 let Tf:=fresh in
 assert (Tf:exists D, (BetS B D A /\ Cong B D A C)) by (conclude proposition_03);destruct Tf as [D];spliter.
(* Goal: False *)
 assert (Cong D B A C) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Out B A D) 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 (nCol A B C) by (conclude_def Triangle ).
(* Goal: False *)
 assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (CongA A B C D B C) by (conclude lemma_equalangleshelper).
(* Goal: False *)
 assert (CongA D B C A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA D B C A C B) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (Cong B D C A) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong B C C B) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert ((Cong D C A B /\ CongA B D C C A B /\ CongA B C D C B A)) by (conclude proposition_04).
(* Goal: False *)
 assert (~ Col C B A).
(* Goal: not (@Col Ax0 B C D) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax0 B C D) *)
  intro.
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (CongA C B A A B C) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (CongA B C D A B C) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (CongA B C D A C B) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (~ Col A C B).
(* Goal: not (@Col Ax0 B C D) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax0 B C D) *)
  intro.
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (CongA A C B B C A) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (CongA B C D B C A) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (CongA B C A B C D) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out C B B) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out C A A) by (conclude lemma_ray4).
(* Goal: False *)
 assert (~ Col B C D).
(* Goal: not (@Col Ax0 B C D) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax0 B C D) *)
  intro.
(* Goal: False *)
  assert (Col B D A) by (conclude_def Col ).
(* Goal: False *)
  assert (Col D B A) by (forward_using lemma_collinearorder).
(* 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: False *)
 assert (CongA B C D B C D) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (LtA B C D B C A) by (conclude_def LtA ).
(* Goal: False *)
 assert (LtA B C A B C A) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: False *)
 assert (~ LtA B C A B C A) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: not (@Lt Ax0 A C A B) *)
close.
Qed.

End Euclid.


