Library GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram
Require Export GeoCoq.Elements.OriginalProofs.proposition_33.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_Playfair.
Section Euclid.
Context `{Ax:euclidean_euclidean}.
Lemma lemma_triangletoparallelogram :
∀ A C D E F,
Par D C E F → Col E F A →
∃ X, PG A X C D ∧ Col E F X.
Proof.
intros.
assert (nCol D C E) by (forward_using lemma_parallelNC).
assert (neq D C) by (forward_using lemma_NCdistinct).
assert (neq C D) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ B, (BetS C D B ∧ Cong D B C D)) by (conclude postulate_extension);destruct Tf as [B];spliter.
assert (BetS B D C) by (conclude axiom_betweennesssymmetry).
assert (nCol C E F) by (forward_using lemma_parallelNC).
assert (neq E F) by (forward_using lemma_NCdistinct).
assert (¬ Col B C A).
{
intro.
assert (Col C D B) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (Col C A D) by (conclude lemma_collinear4).
assert (Col D C A) by (forward_using lemma_collinearorder).
assert (neq C D) by (forward_using lemma_betweennotequal).
assert (Meet D C E F) by (conclude_def Meet ).
assert (¬ Meet D C E F) by (conclude_def Par ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ c b M, (BetS c A b ∧ CongA b A D A D B ∧ CongA b A D B D A ∧ CongA D A b B D A ∧ CongA c A D A D C ∧ CongA c A D C D A ∧ CongA D A c C D A ∧ Par c b B C ∧ Cong c A D C ∧ Cong A b B D ∧ Cong A M M D ∧ Cong c M M C ∧ Cong B M M b ∧ BetS c M C ∧ BetS B M b ∧ BetS A M D)) by (conclude proposition_31);destruct Tf as [c[b[M]]];spliter.
assert (BetS b M B) by (conclude axiom_betweennesssymmetry).
assert (nCol b B C) by (forward_using lemma_parallelNC).
let Tf:=fresh in
assert (Tf:∃ R, (BetS b R D ∧ BetS C R M)) by (conclude postulate_Pasch_inner);destruct Tf as [R];spliter.
assert (BetS C M c) by (conclude axiom_betweennesssymmetry).
assert (BetS C R c) by (conclude lemma_3_6b).
assert (BetS b A c) by (conclude axiom_betweennesssymmetry).
assert (nCol c b C) by (forward_using lemma_parallelNC).
assert (nCol b c C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ Q, (BetS b Q R ∧ BetS C Q A)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.
assert (BetS b Q D) by (conclude lemma_3_6b).
assert (Col C D B) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col B C C) by (conclude_def Col ).
assert (Par c b D C) by (conclude lemma_collinearparallel).
assert (Par D C c b) by (conclude lemma_parallelsymmetric).
assert (Col c A b) by (conclude_def Col ).
assert (Col c b A) by (forward_using lemma_collinearorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col C b b) by (conclude_def Col ).
assert (neq A b) by (forward_using lemma_betweennotequal).
assert (Par D C A b) by (conclude lemma_collinearparallel).
assert (Par A b D C) by (conclude lemma_parallelsymmetric).
assert (Par b A C D) by (forward_using lemma_parallelflip).
assert (Cong B D D B) by (conclude cn_equalityreverse).
assert (Cong A b D B) by (conclude lemma_congruencetransitive).
assert (Cong A b C D) by (conclude lemma_congruencetransitive).
assert (Cong b A C D) by (forward_using lemma_congruenceflip).
assert (BetS A Q C) by (conclude axiom_betweennesssymmetry).
assert ((Par b C A D ∧ Cong b C A D)) by (conclude proposition_33).
assert (Par A b C D) by (forward_using lemma_parallelflip).
assert (Par A D b C) by (conclude lemma_parallelsymmetric).
assert (PG A b C D) by (conclude_def PG ).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col E F E) by (conclude_def Col ).
assert (Col E F F) by (conclude_def Col ).
assert (Col E F b).
by cases on (eq A F ∨ neq A F).
{
assert (neq F E) by (conclude lemma_inequalitysymmetric).
assert (neq A E) by (conclude cn_equalitysub).
assert (Par D C A E) by (conclude lemma_collinearparallel2).
assert (Col A b E) by (conclude lemma_Playfair).
assert (Col F b E) by (conclude cn_equalitysub).
assert (Col E F b) by (forward_using lemma_collinearorder).
close.
}
{
assert (Par D C A F) by (conclude lemma_collinearparallel).
assert (Col A b F) by (conclude lemma_Playfair).
assert (Col A F b) by (forward_using lemma_collinearorder).
assert (Col A F E) by (forward_using lemma_collinearorder).
assert (Col F b E) by (conclude lemma_collinear4).
assert (Col E F b) by (forward_using lemma_collinearorder).
close.
}
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_Playfair.
Section Euclid.
Context `{Ax:euclidean_euclidean}.
Lemma lemma_triangletoparallelogram :
∀ A C D E F,
Par D C E F → Col E F A →
∃ X, PG A X C D ∧ Col E F X.
Proof.
intros.
assert (nCol D C E) by (forward_using lemma_parallelNC).
assert (neq D C) by (forward_using lemma_NCdistinct).
assert (neq C D) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ B, (BetS C D B ∧ Cong D B C D)) by (conclude postulate_extension);destruct Tf as [B];spliter.
assert (BetS B D C) by (conclude axiom_betweennesssymmetry).
assert (nCol C E F) by (forward_using lemma_parallelNC).
assert (neq E F) by (forward_using lemma_NCdistinct).
assert (¬ Col B C A).
{
intro.
assert (Col C D B) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (Col C A D) by (conclude lemma_collinear4).
assert (Col D C A) by (forward_using lemma_collinearorder).
assert (neq C D) by (forward_using lemma_betweennotequal).
assert (Meet D C E F) by (conclude_def Meet ).
assert (¬ Meet D C E F) by (conclude_def Par ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ c b M, (BetS c A b ∧ CongA b A D A D B ∧ CongA b A D B D A ∧ CongA D A b B D A ∧ CongA c A D A D C ∧ CongA c A D C D A ∧ CongA D A c C D A ∧ Par c b B C ∧ Cong c A D C ∧ Cong A b B D ∧ Cong A M M D ∧ Cong c M M C ∧ Cong B M M b ∧ BetS c M C ∧ BetS B M b ∧ BetS A M D)) by (conclude proposition_31);destruct Tf as [c[b[M]]];spliter.
assert (BetS b M B) by (conclude axiom_betweennesssymmetry).
assert (nCol b B C) by (forward_using lemma_parallelNC).
let Tf:=fresh in
assert (Tf:∃ R, (BetS b R D ∧ BetS C R M)) by (conclude postulate_Pasch_inner);destruct Tf as [R];spliter.
assert (BetS C M c) by (conclude axiom_betweennesssymmetry).
assert (BetS C R c) by (conclude lemma_3_6b).
assert (BetS b A c) by (conclude axiom_betweennesssymmetry).
assert (nCol c b C) by (forward_using lemma_parallelNC).
assert (nCol b c C) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ Q, (BetS b Q R ∧ BetS C Q A)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.
assert (BetS b Q D) by (conclude lemma_3_6b).
assert (Col C D B) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col B C C) by (conclude_def Col ).
assert (Par c b D C) by (conclude lemma_collinearparallel).
assert (Par D C c b) by (conclude lemma_parallelsymmetric).
assert (Col c A b) by (conclude_def Col ).
assert (Col c b A) by (forward_using lemma_collinearorder).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (Col C b b) by (conclude_def Col ).
assert (neq A b) by (forward_using lemma_betweennotequal).
assert (Par D C A b) by (conclude lemma_collinearparallel).
assert (Par A b D C) by (conclude lemma_parallelsymmetric).
assert (Par b A C D) by (forward_using lemma_parallelflip).
assert (Cong B D D B) by (conclude cn_equalityreverse).
assert (Cong A b D B) by (conclude lemma_congruencetransitive).
assert (Cong A b C D) by (conclude lemma_congruencetransitive).
assert (Cong b A C D) by (forward_using lemma_congruenceflip).
assert (BetS A Q C) by (conclude axiom_betweennesssymmetry).
assert ((Par b C A D ∧ Cong b C A D)) by (conclude proposition_33).
assert (Par A b C D) by (forward_using lemma_parallelflip).
assert (Par A D b C) by (conclude lemma_parallelsymmetric).
assert (PG A b C D) by (conclude_def PG ).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col E F E) by (conclude_def Col ).
assert (Col E F F) by (conclude_def Col ).
assert (Col E F b).
by cases on (eq A F ∨ neq A F).
{
assert (neq F E) by (conclude lemma_inequalitysymmetric).
assert (neq A E) by (conclude cn_equalitysub).
assert (Par D C A E) by (conclude lemma_collinearparallel2).
assert (Col A b E) by (conclude lemma_Playfair).
assert (Col F b E) by (conclude cn_equalitysub).
assert (Col E F b) by (forward_using lemma_collinearorder).
close.
}
{
assert (Par D C A F) by (conclude lemma_collinearparallel).
assert (Col A b F) by (conclude lemma_Playfair).
assert (Col A F b) by (forward_using lemma_collinearorder).
assert (Col A F E) by (forward_using lemma_collinearorder).
assert (Col F b E) by (conclude lemma_collinear4).
assert (Col E F b) by (forward_using lemma_collinearorder).
close.
}
close.
Qed.
End Euclid.