proposition: Lemma weak_inverse_projection_postulate__bachmann_s_lotschnittaxiom : weak_inverse_projection_postulate -> bachmann_s_lotschnittaxiom.
proof: Proof. intro hrap. apply bachmann_s_lotschnittaxiom_aux. intros A1 A2 B1 B2 C1 C2 D1 D2 Q P R HQP HQR HPerpAB HPerpAC HPerpBD. intros HCol1 HCol2 HCol3 HCol4 HCol5 HCol6 HCop1 HCop2 HCop3 HCop4. assert (HNC : ~ Col P Q R). apply per_not_col; auto; apply perp_per_1, (perp_col4 A1 A2 B1 B2); auto. destruct (angle_bisector P Q R) as [M [HM1 HM2]]; auto. assert (HSuma : SumA P Q M P Q M P Q R). assert_diffs; apply conga3_suma__suma with P Q M M Q R P Q R; CongA; SumA. assert (HAcute : Acute P Q M). { apply nbet_sams_suma__acute with P Q R; auto. intro; apply HNC; Col. assert (LeA P Q M P Q R) by Lea. assert (Per P Q R) by (apply perp_per_2, perp_col2 with A1 A2; Col; apply perp_sym, perp_col2 with B1 B2; Col; Perp). apply sams_lea2__sams with P Q R P Q R; SumA. } destruct (weak_inverse_projection_postulate__bachmann_s_lotschnittaxiom_aux hrap A1 A2 B1 B2 C1 C2 Q P R M) as [HParB [S [HS1 HS2]]]; Col. destruct (weak_inverse_projection_postulate__bachmann_s_lotschnittaxiom_aux hrap B1 B2 A1 A2 D1 D2 Q R P M) as [HParA [T [HT1 HT2]]]; [trivial..|]; [Perp|Cop..|Col| |CongA|]. apply l11_24, HM1. destruct (col_dec C1 C2 T). exists T; split; Col. destruct (col_dec D1 D2 S). exists S; split; Col. assert (HOut : Out Q S T) by (apply l6_7 with M; Out). clear dependent M. destruct HOut as [HSQ [HTQ [HBet|HBet]]]. - assert (HTS : TS C1 C2 R T). { apply l9_8_2 with Q. repeat split; [apply par_not_col with B1 B2; Par| |exists S; split]; Col. apply l12_6, par_strict_col2_par_strict with B1 B2; Par; Col. } destruct HTS as [_ [_ [I [HI1 HI2]]]]. assert (T <> R). intro; treat_equalities; Col. exists I; split; ColR. - assert (HTS : TS D1 D2 P S). { apply l9_8_2 with Q. repeat split; [apply par_not_col with A1 A2; Par| |exists T; split]; Col. apply l12_6, par_strict_col2_par_strict with A1 A2; Par; Col. } destruct HTS as [_ [_ [I [HI1 HI2]]]]. assert (P <> S). intro; treat_equalities; Col. exists I; split; ColR. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.bachmann_s_lotschnittaxiom_variant GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel