proposition: Lemma weak_tarski_s_parallel_postulate__weak_inverse_projection_postulate_aux : weak_tarski_s_parallel_postulate -> forall A B C P T, Per A B C -> InAngle T A B C -> P <> T -> CongA P B A P B C -> Per B P T -> Coplanar A B C P -> (exists X, Out B A X /\ Col T P X) \/ (exists Y, Out B C Y /\ Col T P Y).
proof: Proof. intros tora A B C P T HPer HInAngle HPT HCongA HPerP HCop. assert (HIn : InAngle P A B C) by (apply conga_cop_inangle_per2__inangle with T; assumption). assert (HAcute : Acute P B A) by (apply acute_sym, conga_inangle_per__acute with C; assumption). assert (HAcute' : Acute P B C) by (apply (acute_conga__acute P B A); assumption). assert_diffs. assert (HPerp : Perp B P P T) by (apply per_perp; auto). assert (HNCol : ~ Col A B C) by (apply per_not_col; auto). assert (HNCol1 : ~ Col B P T) by (apply per_not_col; auto). destruct (col_dec A B T). left; exists T; split; Col. apply l6_6, acute_col_perp__out_1 with P; Col. destruct (tora A B C T) as [U [V [HU [HV HUTV]]]]; trivial. destruct (col_dec P T U) as [HCol|HNCol2]. left; exists U; split; Col. destruct (col_dec P T V) as [HCol|HNCol3]. right; exists V; split; Col. destruct (cop__one_or_two_sides P T B U) as [HTS|HOS]; Col; [CopR|..]. - destruct HTS as [_ [_ [X [HX1 HX2]]]]. left; exists X; split; Col. apply l6_7 with U; auto. assert_diffs; apply l6_6, bet_out; auto. intro; subst; apply HNCol1, HX1. - assert (HTS : TS P T B V) by (apply l9_8_2 with U; Side; repeat split; [..|exists T; split]; Col). destruct HTS as [_ [_ [Y [HY1 HY2]]]]. right; exists Y; split; Col. apply l6_7 with V; auto. assert (Y <> B) by (intro; subst; apply HNCol1, HY1). assert_diffs; Out. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel