# Library GeoCoq.Elements.OriginalProofs.lemma_parallelbetween

Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_parallelbetween :

∀ B H K L M,

BetS H B K → Par M B H L → Col L M K →

BetS L M K.

Proof.

intros.

assert (¬ Meet M B H L) by (conclude_def Par ).

assert (nCol M B H) by (forward_using lemma_parallelNC).

assert (nCol M H L) by (forward_using lemma_parallelNC).

assert (neq M B) by (forward_using lemma_NCdistinct).

assert (neq H L) by (forward_using lemma_NCdistinct).

assert (nCol M L H) by (forward_using lemma_NCorder).

assert (Col M L K) by (forward_using lemma_collinearorder).

assert (Col H B K) by (conclude_def Col ).

assert (eq M M) by (conclude cn_equalityreflexive).

assert (eq L L) by (conclude cn_equalityreflexive).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (¬ eq M K).

{

intro.

assert (Col H B M) by (conclude cn_equalitysub).

assert (Col M B H) by (forward_using lemma_collinearorder).

assert (Col H L H) by (conclude_def Col ).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

assert (nCol M L H) by (forward_using lemma_NCorder).

assert (Col M L M) by (conclude_def Col ).

assert (nCol M K H) by (conclude lemma_NChelper).

assert (nCol H M K) by (forward_using lemma_NCorder).

assert ((eq L M ∨ eq L K ∨ eq M K ∨ BetS M L K ∨ BetS L M K ∨ BetS L K M)) by (conclude_def Col ).

assert (BetS L M K).

by cases on (eq L M ∨ eq L K ∨ eq M K ∨ BetS M L K ∨ BetS L M K ∨ BetS L K M).

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (Col M B M) by (conclude_def Col ).

assert (Col H L L) by (conclude_def Col ).

assert (Col H L M) by (conclude cn_equalitysub).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (Col H B L) by (conclude cn_equalitysub).

assert (Col H L B) by (forward_using lemma_collinearorder).

assert (Col M B B) by (conclude_def Col ).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (nCol H K M) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ E, (BetS H E L ∧ BetS M E B)) by (conclude postulate_Pasch_inner);destruct Tf as [E];spliter.

assert (Col H E L) by (conclude_def Col ).

assert (Col M E B) by (conclude_def Col ).

assert (Col H L E) by (forward_using lemma_collinearorder).

assert (Col M B E) by (forward_using lemma_collinearorder).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (BetS M K L) by (conclude axiom_betweennesssymmetry).

let Tf:=fresh in

assert (Tf:∃ E, (BetS H E L ∧ BetS M B E)) by (conclude postulate_Pasch_outer);destruct Tf as [E];spliter.

assert (Col H E L) by (conclude_def Col ).

assert (Col M B E) by (conclude_def Col ).

assert (Col H L E) by (forward_using lemma_collinearorder).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_parallelbetween :

∀ B H K L M,

BetS H B K → Par M B H L → Col L M K →

BetS L M K.

Proof.

intros.

assert (¬ Meet M B H L) by (conclude_def Par ).

assert (nCol M B H) by (forward_using lemma_parallelNC).

assert (nCol M H L) by (forward_using lemma_parallelNC).

assert (neq M B) by (forward_using lemma_NCdistinct).

assert (neq H L) by (forward_using lemma_NCdistinct).

assert (nCol M L H) by (forward_using lemma_NCorder).

assert (Col M L K) by (forward_using lemma_collinearorder).

assert (Col H B K) by (conclude_def Col ).

assert (eq M M) by (conclude cn_equalityreflexive).

assert (eq L L) by (conclude cn_equalityreflexive).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (¬ eq M K).

{

intro.

assert (Col H B M) by (conclude cn_equalitysub).

assert (Col M B H) by (forward_using lemma_collinearorder).

assert (Col H L H) by (conclude_def Col ).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

assert (nCol M L H) by (forward_using lemma_NCorder).

assert (Col M L M) by (conclude_def Col ).

assert (nCol M K H) by (conclude lemma_NChelper).

assert (nCol H M K) by (forward_using lemma_NCorder).

assert ((eq L M ∨ eq L K ∨ eq M K ∨ BetS M L K ∨ BetS L M K ∨ BetS L K M)) by (conclude_def Col ).

assert (BetS L M K).

by cases on (eq L M ∨ eq L K ∨ eq M K ∨ BetS M L K ∨ BetS L M K ∨ BetS L K M).

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (Col M B M) by (conclude_def Col ).

assert (Col H L L) by (conclude_def Col ).

assert (Col H L M) by (conclude cn_equalitysub).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (Col H B L) by (conclude cn_equalitysub).

assert (Col H L B) by (forward_using lemma_collinearorder).

assert (Col M B B) by (conclude_def Col ).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (nCol H K M) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ E, (BetS H E L ∧ BetS M E B)) by (conclude postulate_Pasch_inner);destruct Tf as [E];spliter.

assert (Col H E L) by (conclude_def Col ).

assert (Col M E B) by (conclude_def Col ).

assert (Col H L E) by (forward_using lemma_collinearorder).

assert (Col M B E) by (forward_using lemma_collinearorder).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

{

close.

}

{

assert (¬ ¬ BetS L M K).

{

intro.

assert (BetS M K L) by (conclude axiom_betweennesssymmetry).

let Tf:=fresh in

assert (Tf:∃ E, (BetS H E L ∧ BetS M B E)) by (conclude postulate_Pasch_outer);destruct Tf as [E];spliter.

assert (Col H E L) by (conclude_def Col ).

assert (Col M B E) by (conclude_def Col ).

assert (Col H L E) by (forward_using lemma_collinearorder).

assert (Meet M B H L) by (conclude_def Meet ).

contradict.

}

close.

}

close.

Qed.

End Euclid.