proposition: Lemma greenberg__aristotle : greenberg_s_axiom -> aristotle_s_axiom.
proof: Proof. intros HG P Q A B C HNC HAcute. destruct (l10_15 A B B C) as [D' [HPerp1 HOS1]]; Col. elim (eq_dec_points P Q); intro HPQ; treat_equalities. { destruct (l8_18_existence A B C) as [X [HCol HPerp]]; Col; exists X, C. split; [apply l6_6, acute_col_perp__out with C; try apply acute_sym; finish|]. split; [apply out_trivial; assert_diffs; auto|]. split; [|apply lt1123; assert_diffs; auto]. elim (eq_dec_points X B); intro HBX; treat_equalities; Perp. apply perp_per_1, perp_col2 with A B; Col. } { destruct (segment_construction_3 B D' P Q) as [P' [HOut1 HCong1]]; try solve [assert_diffs; auto]. destruct (HG P' B A A B C) as [C' HC']; Col; try solve [assert_diffs; auto]; [apply perp_per_2, perp_col2 with D' B; finish; assert_diffs; auto|]. destruct HC' as [HLtA HOut2]. destruct (l10_15 B C' C' C) as [D'' [HPerp2 HOS2]]; Col; try (intro H; apply HNC; assert_diffs; assert_cols; ColR). destruct (segment_construction_3 C' D'' P Q) as [P'' [HOut3 HCong2]]; try solve [assert_diffs; auto]. destruct (segment_construction_3 B C B P'') as [Z [HOut4 HCong3]]; try (intro; treat_equalities; assert_cols; Col); [elim (perp_not_col2 _ _ _ _ HPerp2); intro HF; apply HF; Col|]. destruct (l8_18_existence A B Z) as [Z' [HCol HPerp3]]; [intro; apply HNC; ColR|]; assert (HOut5 : Out B Z' A). { apply acute_col_perp__out with Z; finish. apply acute_sym, acute_out2__acute with A C; finish. apply out_trivial; assert_diffs; auto. } exists Z', Z; do 2 (split; finish); split; [apply perp_per_1, perp_col2 with A B; assert_diffs; Col|]. apply cong2_lt__lt with C' P'' Z' Z; Cong. apply cong_lt_per2__lt_1 with B B; Cong; try (apply perp_per_1); [apply perp_col2 with A B|apply perp_col2_bis with C' D''|]; try solve [assert_diffs; Col; Perp]. assert (HCongA : CongA B C' P' A B P''). { apply l11_10 with B P' C' P''; try solve [assert_diffs; finish]. apply l11_49; try solve [assert_diffs; finish]; eCong. apply l11_16; try solve [assert_diffs; auto]; apply perp_per_1; [apply perp_col2 with B D'|apply perp_col2 with C' D'']; assert_diffs; finish; apply perp_sym; apply perp_col2 with B A; finish. } assert (HT : InAngle P'' Z' B Z). { apply l11_25 with P'' A C; finish; [|apply out_trivial; intro]; [|treat_equalities; elim (perp_not_col2 _ _ _ _ HPerp3); Col]. apply lea_in_angle. { apply l11_30 with B C' P' A B C; finish; apply conga_refl; assert_diffs; auto. } { apply one_side_transitivity with D''. apply col2_os__os with B C'; assert_diffs; finish. apply out_one_side_1 with C'; finish. elim (perp_not_col2 _ _ _ _ HPerp2); intro HF; Col. intro; apply HF; ColR. } } destruct HT as [_ [_ [_ [T [HBet1 [?|HOut6]]]]]]; treat_equalities; [exfalso; apply HNC; ColR|destruct HOut6 as [_ [_ HOut6]]]. assert (HPar : Par Z Z' C' P''). { apply l12_9 with B C'; Cop; [|apply col__coplanar; ColR|apply perp_sym|]; [|apply perp_col2 with A B; assert_diffs; finish| apply perp_col2 with C' D''; assert_diffs; finish]. assert (Coplanar B Z C C') by (apply col__coplanar; ColR). assert (Coplanar C' P'' D'' B) by (apply col__coplanar; ColR). assert (Coplanar C' B D'' C); [Cop|CopR]. } assert (HTZ : T <> Z). { intro; treat_equalities; destruct HLtA as [_ HF]; apply HF. apply conga_trans with A B P''; finish. apply conga_sym, out2__conga; [assert_diffs; finish|]. apply l6_7 with T; finish. assert_diffs; split; auto; split; auto. induction HOut6; auto. } assert (HTZ' : T <> Z'). { intro; treat_equalities; elim (perp_not_col2 _ _ _ _ HPerp2); Col. intro HF; apply HF; induction HOut6; ColR. } assert (HTP'' : T <> P''). { intro; treat_equalities; assert (HF : Acute B T Z). { apply cong__acute; try solve [assert_diffs; finish]. } apply (acute__not_obtuse _ _ _ HF). apply acute_suppa__obtuse with B T Z'; try (apply suppa_left_comm, bet__suppa); try solve [assert_diffs; finish]. apply acute_sym, l11_43; try solve [assert_diffs; auto]; left. apply perp_per_1; apply perp_col2 with A B; Col; [|assert_diffs; auto]. apply perp_sym, perp_col2 with Z Z'; finish. } assert (HBet2 : Bet B T P''); [|clear HOut6]. { elim HOut6; [auto|clear HOut6; intro HF; exfalso]. assert (HObtuse : Obtuse Z T B). { apply acute_suppa__obtuse with B T Z'; try (apply suppa_left_comm, suppa_right_comm); try (apply bet__suppa); try solve [assert_diffs; finish]. apply acute_sym, l11_43; try solve [assert_diffs; auto]; left. apply perp_per_1; apply perp_col2 with A B; Col; [|assert_diffs; auto]. apply perp_sym, perp_col2 with Z Z'; finish. } apply (not_and_lta B Z T B T Z); split. { apply acute_obtuse__lta; [|apply obtuse_sym; auto]. apply acute_sym, l11_43; assert_diffs; finish. right; apply obtuse_sym; auto. } { apply l11_44_2_a; [intro; apply HNC; ColR|]. apply le1234_lt__lt with B P''; [apply cong__le; finish|]. apply bet__lt1213; assert_diffs; finish. } } apply par_symmetry in HPar; apply (par_not_col_strict _ _ _ _ T) in HPar; Col; [|intro; apply HTP'', l6_21 with C' P'' B T; Col; [|intro; treat_equalities; apply HNC; ColR]; elim (perp_not_col2 _ _ _ _ HPerp2); Col; intros HF ?; apply HF; ColR]. assert (HOS3 := pars__os3412 _ _ _ _ HPar). assert (HOut6 : Out P'' T B) by (split; [auto|split; assert_diffs; finish]). assert (HOut7 : Out B C' Z') by (apply l6_7 with A; finish). destruct HOut7 as [_ [_ [HBet3|HBet3]]]; [|apply bet__lt1213; Between; intro; treat_equalities; apply par_strict_not_col_1 in HPar; Col; apply one_side_not_col123 in HOS3; Col]. exfalso; apply (l9_9_bis _ _ _ _ HOS3), l9_8_2 with B. { split; [intro; apply HNC; ColR|]. split; [intro; apply HNC; ColR|]. exists T; split; finish. } { apply out_one_side_1 with Z'; finish; [intro; apply HNC; ColR|]. assert_diffs; do 2 (split; auto); right; finish. } } Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri