# 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.

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.