Library GeoCoq.Elements.OriginalProofs.lemma_lessthantransitive

Require Export GeoCoq.Elements.OriginalProofs.lemma_layoff.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray4.
Require Export GeoCoq.Elements.OriginalProofs.lemma_layoffunique.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_lessthantransitive :
   ∀ A B C D E F,
   Lt A B C D → Lt C D E F →
   Lt A B E F.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ G, (BetS C G D ∧ Cong C G A B)) by (conclude_def Lt );destruct Tf as [G];spliter.
rename_H H;
let Tf:=fresh in
assert (Tf:∃ H, (BetS E H F ∧ Cong E H C D)) by (conclude_def Lt );destruct Tf as [H];spliter.
assert (neq E H) by (forward_using lemma_betweennotequal).
assert (neq C G) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ K, (Out E H K ∧ Cong E K C G)) by (conclude lemma_layoff);destruct Tf as [K];spliter.
assert (Cong E K A B) by (conclude lemma_congruencetransitive).
assert ((BetS E K H ∨ eq H K ∨ BetS E H K)) by (conclude lemma_ray1).
assert (BetS E K H).
by cases on (BetS E K H ∨ eq H K ∨ BetS E H K).
{
 close.
 }
{
 assert (Cong C G E K) by (conclude lemma_congruencesymmetric).
 assert (Cong C G E H) by (conclude cn_equalitysub).
 assert (Cong C G C D) by (conclude lemma_congruencetransitive).
 assert (Out C G D) by (conclude lemma_ray4).
 assert (eq G G) by (conclude cn_equalityreflexive).
 assert (Out C G G) by (conclude lemma_ray4).
 assert (¬ ¬ BetS E K H).
  {
  intro.
  assert (eq G D) by (conclude lemma_layoffunique).
  assert (neq G D) by (forward_using lemma_betweennotequal).
  contradict.
  }
 close.
 }
{
 assert (Cong C D E H) by (conclude lemma_congruencesymmetric).
 assert (Cong C G E K) by (conclude lemma_congruencesymmetric).
 assert (neq C D) by (forward_using lemma_betweennotequal).
 assert (neq H K) by (forward_using lemma_betweennotequal).
 let Tf:=fresh in
 assert (Tf:∃ J, (BetS C D J ∧ Cong D J H K)) by (conclude postulate_extension);destruct Tf as [J];spliter.
 assert (Out C D J) by (conclude lemma_ray4).
 assert (Out C D G) by (conclude lemma_ray4).
 assert (Cong C J E K) by (conclude lemma_sumofparts).
 assert (Cong C J C G) by (conclude lemma_congruencetransitive).
 assert (eq J G) by (conclude lemma_layoffunique).
 assert (BetS G D J) by (conclude lemma_3_6a).
 assert (¬ ¬ BetS E K H).
  {
  intro.
  assert (neq G J) by (forward_using lemma_betweennotequal).
  assert (neq J G) by (conclude lemma_inequalitysymmetric).
  contradict.
  }
 close.
 }

assert (BetS E K F) by (conclude lemma_3_6b).
assert (Lt A B E F) by (conclude_def Lt ).
close.
Qed.

End Euclid.