proposition: Lemma alternate_interior__proclus : greenberg_s_axiom -> alternate_interior_angles_postulate -> proclus_postulate.
proof: Proof. intros greenberg aia. intros A B C D P Q HPar HP HQ HCop. elim(col_dec C D P). intro HConf; exists P; split; Col. intro HStrict. assert(HParS : Par_strict A B C D). { apply par_strict_symmetry, par_not_col_strict with P; auto. apply par_symmetry, HPar. } destruct (l8_18_existence C D P) as [C0 []]; auto. destruct (col_dec P Q C0) as [|HNCol1]. exists C0; split; auto. assert_diffs. assert(HQ1 : exists Q1, Col Q P Q1 /\ OS A B C0 Q1). { apply cop_not_par_same_side with P; Col. apply not_col_permutation_1, (par_not_col C D); Col; Par. apply coplanar_pseudo_trans with C D P; trivial; apply coplanar_perm_1; [apply col_cop__cop with B|apply col_cop__cop with A; Col|]; Cop. } destruct HQ1 as [Q1 [HCol1 HOS1]]. assert(P<>Q1) by (intro; subst; apply one_side_not_col124 in HOS1; apply HOS1, HP). assert(~ Col P C0 Q1) by (intro; apply HNCol1; ColR). assert(HA1 : exists A1, Col A B A1 /\ OS P C0 Q1 A1). { destruct (col_dec P C0 A). - destruct (cop_not_par_same_side P C0 B A P Q1) as [A1 []]; Col. intro; apply HParS; exists C0; split; ColR. apply coplanar_perm_19, col_cop__cop with A; Col; Cop. exists A1; split; Col. - apply (cop_not_par_same_side _ _ _ _ P); Col. apply coplanar_perm_19, col_cop__cop with B; Cop. } destruct HA1 as [A1 []]. assert(HC1 : exists C1, Col C D C1 /\ OS P C0 Q1 C1). { assert (Coplanar C D P Q1) by (apply col_cop__cop with Q; Col). destruct (perp_not_col2 P C0 C D); Perp. apply (cop_not_par_same_side _ _ _ _ C0); Col. apply coplanar_perm_5, col_cop__cop with D; Cop. destruct (cop_not_par_same_side P C0 D C C0 Q1) as [C1 []]; Col. apply coplanar_perm_5, col_cop__cop with C; Col; Cop. exists C1; split; Col. } destruct HC1 as [C1 []]. assert_diffs. destruct (alternate_interior__proclus_aux greenberg aia A1 C0 C1 P Q1) as [Y []]; auto. apply (par_strict_col4__par_strict A B C D); auto. apply (perp_col2 C D); auto. apply (col2_os__os A B); auto. clear dependent A. exists Y; split; ColR. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel