proposition: Lemma alternate_interior__proclus_aux : greenberg_s_axiom -> alternate_interior_angles_postulate -> forall A C D P Q, Par_strict P A C D -> Perp C D P C -> OS P A C Q -> OS P C Q A -> OS P C Q D -> exists Y, Col P Q Y /\ Col C D Y.
proof: Proof. intros greenberg aia. intros A C D P Q HParS HPerp HOS1 HOS2 HOS3. destruct (symmetric_point_construction D C) as [D' []]. assert_diffs. assert (~ Col P A Q) by (apply one_side_not_col124 with C, HOS1). assert (~ Col P C Q) by (apply one_side_not_col123 with D, HOS3). assert (~ Col P C D) by (apply one_side_not_col124 with Q, HOS3). assert (LtA A P Q A P C) by (apply inangle__lta; [Col|Side]). assert (OS P C D A) by (apply one_side_transitivity with Q; Side). assert (Acute A P Q). { exists A, P, C; split; auto. apply (l11_17 P C D'). apply per_col with D; Col; Perp. apply conga_sym, conga_right_comm, aia; [|apply par_col_par with D; Par; Col]. apply l9_8_2 with D; trivial. apply invert_two_sides, bet__ts; Col. } destruct (greenberg P C D A P Q) as [S [HS1 HS2]]; Perp; Col. assert (OS P C S D) by (apply invert_one_side, out_one_side; Col). assert (HY : InAngle Q C P S). { apply os2__inangle. apply one_side_transitivity with D; Side. exists A. assert (OS P C S A). apply one_side_transitivity with D; Side. assert (Par_strict P A S C). { apply lta_distincts in HS1; spliter. apply par_strict_right_comm, par_strict_col_par_strict with D; Col. } assert (HTS : TS P S C A) by (apply l9_31; Side). split; trivial. assert (CongA A P S C S P) by (apply aia; [Side|Par]). assert (HLta : LtA A P S A P Q) by (apply (conga_preserves_lta P S C A P Q); CongA). destruct HLta as [HLea HNConga]. apply invert_two_sides, in_angle_two_sides; [|destruct HTS as [_ []]; Col|]. { intro. assert (Out P Q S). apply col_one_side_out with C; [|apply one_side_transitivity with A]; Side. apply HNConga, out2__conga; Out. } apply l11_24, lea_in_angle; trivial. apply one_side_transitivity with C; Side. } clear dependent A. destruct HY as [_ [_ [_ [Y [HY1 HY2]]]]]. exists Y; split; [|ColR]. destruct HY2; [subst|]; Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel