proposition: Lemma aristotle__greenberg : aristotle_s_axiom -> greenberg_s_axiom.
proof: Proof. intros aristotle P Q R A B C. intros HNColB HABCacute HQRdiff HQright. elim (eq_dec_points P Q); intro HPQdiff. { treat_equalities. assert_diffs. exists R. split; [|apply out_trivial; auto]. split. apply lea121345; auto. intro. apply HNColB. apply col_permutation_4. apply out_col. apply (eq_conga_out P R); auto. } assert (HXY : (exists X Y, Out B A X /\ Out B C Y /\ Per B X Y /\ Lt P Q X Y)) by (apply aristotle; assumption). destruct HXY as [X [Y [PX [PY [HXright [Hle HNcong]]]]]]. assert_diffs. assert (HXYdiff : X <> Y) by (intro; treat_equalities; auto). assert (HT : (exists T, Out Q T P /\ Cong Q T X Y)) by (apply l6_11_existence; auto). destruct HT as [T []]. assert (HS : (exists S, Out Q S R /\ Cong Q S X B)) by (apply l6_11_existence; auto). destruct HS as [S []]. assert_diffs. exists S. split; auto. assert (Per S Q P) by (apply (l8_3 R); Perp; Col). assert (Per T Q S) by (apply (l8_3 P); Perp; Col). assert (P<>S). { intro; treat_equalities. assert (P=Q) by (apply l8_8; auto); treat_equalities; absurde. } assert (T<>S). { intro; treat_equalities. assert (T=Q) by (apply l8_8; auto); treat_equalities; absurde. } apply conga_preserves_lta with P S Q T S Q; try (apply conga_refl; auto); [|split]. - apply conga_trans with X B Y; [|apply out2__conga; auto]. assert (HInter : (Cong T S Y B /\ (T <> S -> CongA Q T S X Y B /\ CongA Q S T X B Y))). { apply (l11_49 T Q S Y X B); Cong. apply l11_16; Perp. } destruct HInter as [_ [_ HConga]]; auto. apply conga_left_comm; auto. - apply lea_comm. apply (l11_29_b Q S P Q S T). exists T. split; CongA. repeat split; auto. exists P. split; [|right; apply out_trivial; auto]. apply l6_13_1. apply l6_6; auto. apply (le_transitivity Q P X Y). apply (le_transitivity Q P P Q); Le. apply (cong__le); Cong. - intro HConga. assert (HInter : Cong Q P Q T /\ Cong S P S T /\ CongA Q P S Q T S). { apply l11_50_1; Cong. { intro. assert (HUn : S=Q\/P=Q) by (apply l8_9; Col). destruct HUn; treat_equalities; absurde. } apply l11_16; Perp. CongA. } destruct HInter as [HCong _]. apply HNcong. apply (cong_transitivity P Q T Q); Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri