proposition: Lemma universal_posidonius_postulate__perpendicular_transversal_postulate_aux : universal_posidonius_postulate -> forall E F G H R P, Perp E G R P -> Coplanar F H P R -> Col E G R -> Saccheri E F H G -> Perp F H P R.
proof: Proof. intros HP E F G H R P HPerp HCop HCol HSacc. assert (HPerp1 : Perp E G E F) by (apply perp_sym, sac__perp1214 with H, HSacc). assert (HPar : Par_strict E G F H) by (apply sac__pars1423, HSacc). assert_diffs. assert (HRAH : postulate_of_right_saccheri_quadrilaterals). { destruct (midpoint_existence E G) as [M1 HM1]. destruct (midpoint_existence F H) as [M2 HM2]. assert (HLamb := mid2_sac__lam6521 _ _ _ _ _ _ HSacc HM2 HM1). unfold Lambert in HLamb; spliter. assert (Saccheri M1 M2 F E). { repeat split; Perp. apply cong_symmetry, cong_left_commutativity, HP with E G F H; Col; Par. apply perp_col2 with E M1; Perp; Col. apply l12_6, (par_strict_col4__par_strict E G F H); Col. } apply per_sac__rah with M1 M2 F E; auto. } destruct (eq_dec_points E R) as [|HER]. { subst R. assert (Col F P E) by (apply (cop_per2__col G); Perp; CopR). apply perp_sym, perp_left_comm, perp_col with F; Col. apply per_perp; auto; apply HRAH with G, HSacc. } assert (HP' : forall A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD, IAB <> IAC -> IAB <> IBD -> Perp A1 A2 B1 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 D1 D2 -> Col A1 A2 IAB -> Col B1 B2 IAB -> Col A1 A2 IAC -> Col C1 C2 IAC -> Col B1 B2 IBD -> Col D1 D2 IBD -> Coplanar IAB IAC IBD C1 -> Coplanar IAB IAC IBD C2 -> Coplanar IAB IAC IBD D1 -> Coplanar IAB IAC IBD D2 -> exists I, Col C1 C2 I /\ Col D1 D2 I). { apply bachmann_s_lotschnittaxiom_aux. apply weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom. apply thales_converse_postulate__weak_triangle_circumscription_principle. apply thales_postulate__thales_converse_postulate. apply rah__thales_postulate; assumption. } assert (Coplanar F H E R) by (apply col_cop__cop with G; Col; Cop). assert (~ Col F H R) by (intro; apply HPar; exists R; split; Col). destruct (HP' E G E F P R F H E R F) as [S [HC7 HC8]]; Col; [Perp| |CopR|Cop..|]. apply HRAH in HSacc; Perp. assert (S <> R) by (intro; apply HPar; exists R; subst; split; Col). assert (HSacc2 : Saccheri E F S R). { repeat split. apply per_col with G; Perp; Col. apply perp_per_1; apply (perp_col4 E G R P); Col. apply cong_right_commutativity, HP with E G F H; Col; Par. apply perp_sym, perp_col with P; Perp; Col. apply l12_6, par_strict_col_par_strict with H; Col; [|apply par_strict_symmetry, par_strict_col_par_strict with G; Col; Par]. intro; treat_equalities. assert (~ Col G E F) by (apply per_not_col; Perp). assert (Col E P R) by (apply col_cop2_perp2__col with F E G; Perp; Col; Cop). apply HER, l6_21 with E G F E; ColR. } assert_diffs. apply perp_col with S; Col. assert (Hd := HSacc2). apply sac_distincts in Hd; spliter. apply perp_sym, perp_comm, perp_col with S; Col. apply per_perp; auto. apply HRAH with E, sac_perm, HSacc2. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_variant GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch12_parallel