Require Export GeoCoq.Elements.OriginalProofs.proposition_19.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_legsmallerhypotenuse : 
   forall A B C, 
   Per A B C ->
   Lt A B A C /\ Lt B C A C.
Proof.
(* Goal: forall (A B C : @Point Ax) (_ : @Per Ax A B C), and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
intros.
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Per C B A) by (conclude lemma_8_2).
let Tf:=fresh in
assert (Tf:exists D, (BetS C B D /\ Cong C B D B /\ Cong C A D A /\ neq B A)) by (conclude_def Per );destruct Tf as [D];spliter.
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (nCol A B C) by (conclude lemma_rightangleNC).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Triangle A B C) by (conclude_def Triangle ).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (~ Col A C B).
(* Goal: not (@Col Ax C B A) *)
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
 {
(* Goal: not (@Col Ax C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Triangle A C B) by (conclude_def Triangle ).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert ((LtA C A B A B D /\ LtA B C A A B D)) by (conclude proposition_16).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (~ eq B C).
(* Goal: not (@Col Ax C B A) *)
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
 {
(* Goal: not (@Col Ax C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: False *)
assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Out B C C) by (conclude lemma_ray4).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Out B D D) by (conclude lemma_ray4).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Cong B A B A) by (conclude cn_congruencereflexive).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Cong B D B C) by (forward_using lemma_doublereverse).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Cong A D A C) by (forward_using lemma_doublereverse).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (~ Col A B D).
(* Goal: not (@Col Ax C B A) *)
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
 {
(* Goal: not (@Col Ax C B A) *)
 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 A) 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 A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (CongA A B D A B C) by (conclude_def CongA ).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (CongA A B C A B D) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (LtA B C A A B C) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Lt A B A C) by (conclude proposition_19).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (LtA C A B A B C) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (~ Col B A C).
(* Goal: not (@Col Ax C B A) *)
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
 {
(* Goal: not (@Col Ax C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (CongA B A C C A B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (LtA B A C A B C) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (~ Col C B A).
(* Goal: not (@Col Ax C B A) *)
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
 {
(* Goal: not (@Col Ax C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Triangle C B A) by (conclude_def Triangle ).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (CongA C B A A B C) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (LtA B A C C B A) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Lt C B C A) by (conclude proposition_19).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Cong C B B C) by (conclude cn_equalityreverse).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Lt B C C A) by (conclude lemma_lessthancongruence2).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Cong C A A C) by (conclude cn_equalityreverse).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
assert (Lt B C A C) by (conclude lemma_lessthancongruence).
(* Goal: and (@Lt Ax A B A C) (@Lt Ax B C A C) *)
close.
Qed.

End Euclid.


