Library GeoCoq.Meta_theory.Parallel_postulates.inverse_projection_postulate_proclus_bis
Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch13_1.
Section inverse_projection_postulate_proclus_bis.
Context `{T2D:Tarski_2D}.
Lemma inverse_projection_postulate__proclus_bis : inverse_projection_postulate → alternative_proclus_postulate.
Proof.
intros ip A B C D P Q HPerp2 HInter HNCol.
elim(Col_dec C D P).
intro; ∃ P; split; Col.
intro HNCol1.
assert(Par_strict C D A B).
{ apply (par_not_col_strict _ _ _ _ P); auto.
apply par_symmetry.
apply (perp2_par _ _ _ _ P); auto.
}
destruct HPerp2 as [P1 [P2 [HP [HPerpAP HPerpCP]]]].
assert(HC0 := HPerpCP); auto.
destruct HC0 as [C0 [_ [_ [HC0P [HC0C _]]]]].
assert(HP' := HPerpAP); auto.
destruct HP' as [P' HPerpP].
assert(P'=P) by (apply (l8_14_2_1b _ P1 P2 A B); Col).
subst P'.
destruct HPerpP as [_ [_ [HPP _]]].
assert(P≠C0) by (intro; subst C0; Col).
apply (perp_col0 _ _ _ _ P C0) in HPerpAP; Col.
apply (perp_col0 _ _ _ _ P C0) in HPerpCP; Col.
clear dependent P1.
clear dependent P2.
assert(P≠Q) by (intro; subst; auto).
elim(Col_dec P Q C0).
intro; ∃ C0; Col.
intro HNCol2.
assert(HNCol3 : ¬ Col C0 A B) by (apply (par_not_col C D); auto).
assert(HQ0 := not_par_same_side A B Q P P C0).
destruct HQ0 as [Q0 []]; Col.
assert(HNCol4 : ¬ Col A B Q0) by (apply (one_side_not_col123 _ _ _ C0); Side).
assert(P≠Q0) by (intro; subst; auto).
assert(HNCol5 : ¬ Col P C0 Q0) by (intro; apply HNCol2; ColR).
assert_diffs.
assert(HC1 : ∃ C1, Col C D C1 ∧ C1 ≠ C0).
{ elim(eq_dec_points C C0).
intro; subst C0; ∃ D; split; Col.
intro; ∃ C; split; Col.
}
destruct HC1 as [C1 []].
assert(HA0 : ∃ A0, Col A B A0 ∧ OS P C0 Q0 A0).
{ elim(Col_dec P C0 A).
- intro.
assert(¬ Col P C0 B) by (intro; apply HNCol3; ColR).
assert (HA0 := not_par_same_side P C0 B A P Q0).
destruct HA0 as [A0 []]; Col.
∃ A0.
split; Col.
- intro.
apply (not_par_same_side _ _ _ _ P); Col.
}
destruct HA0 as [A0 []].
assert(HNCol6 : ¬ Col P C0 A0) by (apply (one_side_not_col123 _ _ _ Q0); Side).
assert_diffs.
assert(HY := ip C0 P Q0 C0 C1).
destruct HY as [Y []]; auto.
{
∃ C0, P, A0; split.
assert(HPer := l8_16_1 A B C0 A0 P); destruct HPer; Col; Perp.
split.
{
∃ Q0; split; CongA.
apply os2__inangle; Side.
apply (col2_os__os A B); auto.
}
{
intro.
assert(Habs := conga__or_out_ts C0 P Q0 A0).
destruct Habs as [Habs|Habs]; auto.
apply HNCol4; ColR.
apply l9_9 in Habs; apply Habs; Side.
}
}
{
apply out_trivial; auto.
}
{
assert(HPer := l8_16_1 C D P C1 C0); destruct HPer; Col; Perp.
}
{
∃ Y; split; assert_diffs; ColR.
}
Qed.
End inverse_projection_postulate_proclus_bis.
Require Import GeoCoq.Tarski_dev.Ch13_1.
Section inverse_projection_postulate_proclus_bis.
Context `{T2D:Tarski_2D}.
Lemma inverse_projection_postulate__proclus_bis : inverse_projection_postulate → alternative_proclus_postulate.
Proof.
intros ip A B C D P Q HPerp2 HInter HNCol.
elim(Col_dec C D P).
intro; ∃ P; split; Col.
intro HNCol1.
assert(Par_strict C D A B).
{ apply (par_not_col_strict _ _ _ _ P); auto.
apply par_symmetry.
apply (perp2_par _ _ _ _ P); auto.
}
destruct HPerp2 as [P1 [P2 [HP [HPerpAP HPerpCP]]]].
assert(HC0 := HPerpCP); auto.
destruct HC0 as [C0 [_ [_ [HC0P [HC0C _]]]]].
assert(HP' := HPerpAP); auto.
destruct HP' as [P' HPerpP].
assert(P'=P) by (apply (l8_14_2_1b _ P1 P2 A B); Col).
subst P'.
destruct HPerpP as [_ [_ [HPP _]]].
assert(P≠C0) by (intro; subst C0; Col).
apply (perp_col0 _ _ _ _ P C0) in HPerpAP; Col.
apply (perp_col0 _ _ _ _ P C0) in HPerpCP; Col.
clear dependent P1.
clear dependent P2.
assert(P≠Q) by (intro; subst; auto).
elim(Col_dec P Q C0).
intro; ∃ C0; Col.
intro HNCol2.
assert(HNCol3 : ¬ Col C0 A B) by (apply (par_not_col C D); auto).
assert(HQ0 := not_par_same_side A B Q P P C0).
destruct HQ0 as [Q0 []]; Col.
assert(HNCol4 : ¬ Col A B Q0) by (apply (one_side_not_col123 _ _ _ C0); Side).
assert(P≠Q0) by (intro; subst; auto).
assert(HNCol5 : ¬ Col P C0 Q0) by (intro; apply HNCol2; ColR).
assert_diffs.
assert(HC1 : ∃ C1, Col C D C1 ∧ C1 ≠ C0).
{ elim(eq_dec_points C C0).
intro; subst C0; ∃ D; split; Col.
intro; ∃ C; split; Col.
}
destruct HC1 as [C1 []].
assert(HA0 : ∃ A0, Col A B A0 ∧ OS P C0 Q0 A0).
{ elim(Col_dec P C0 A).
- intro.
assert(¬ Col P C0 B) by (intro; apply HNCol3; ColR).
assert (HA0 := not_par_same_side P C0 B A P Q0).
destruct HA0 as [A0 []]; Col.
∃ A0.
split; Col.
- intro.
apply (not_par_same_side _ _ _ _ P); Col.
}
destruct HA0 as [A0 []].
assert(HNCol6 : ¬ Col P C0 A0) by (apply (one_side_not_col123 _ _ _ Q0); Side).
assert_diffs.
assert(HY := ip C0 P Q0 C0 C1).
destruct HY as [Y []]; auto.
{
∃ C0, P, A0; split.
assert(HPer := l8_16_1 A B C0 A0 P); destruct HPer; Col; Perp.
split.
{
∃ Q0; split; CongA.
apply os2__inangle; Side.
apply (col2_os__os A B); auto.
}
{
intro.
assert(Habs := conga__or_out_ts C0 P Q0 A0).
destruct Habs as [Habs|Habs]; auto.
apply HNCol4; ColR.
apply l9_9 in Habs; apply Habs; Side.
}
}
{
apply out_trivial; auto.
}
{
assert(HPer := l8_16_1 C D P C1 C0); destruct HPer; Col; Perp.
}
{
∃ Y; split; assert_diffs; ColR.
}
Qed.
End inverse_projection_postulate_proclus_bis.