proposition: Lemma t22_24 : archimedes_axiom -> aristotle_s_axiom.
proof: Proof. intros Harchi P Q D A B0 HNCol HACute0. destruct (l8_18_existence A D B0) as [C0 [HColD HPerpD]]; Col. assert (HAC0 : A <> C0) by (intro; subst C0; apply (acute_not_per D A B0); Perp). assert (HNCol0 : ~ Col A B0 C0) by (intro; apply HNCol; ColR). assert (HPerp0 := perp_col A D B0 C0 C0 HAC0 HPerpD HColD). elim (eq_dec_points P Q); intro HPQ. { subst Q; exists C0; exists B0; split; assert_diffs. apply l6_6, acute_col_perp__out with B0; trivial; apply acute_sym; trivial. split. apply out_trivial; auto. repeat split; Perp; Le. intro; treat_equalities; auto. } destruct (segment_construction P Q P Q) as [Q' [HBetQ HCongQ]]. destruct (reach__ex_gradexp_le B0 C0 P Q') as [E [HGE HLe]]. assert_diffs; apply Harchi; trivial. destruct (t22_24_aux1 A B0 C0 E) as [B [C [HGE2 [HPerp HCol]]]]; trivial. assert(HOut : Out A B0 B). apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE2; assert_diffs; apply bet_out; auto. assert(HAcute : Acute D A B). apply (acute_conga__acute D A B0); trivial. apply l6_6 in HOut. assert_diffs; apply out2__conga; auto; apply out_trivial; auto. assert (HAC : A <> C) . intro; subst C; assert_diffs; apply (acute_not_per D A B); trivial. apply perp_per_1, perp_col with C0; Col. exists C, B; split. assert_diffs; apply l6_6, acute_col_perp__out with B; [apply acute_sym; trivial|ColR|apply perp_col with C0; Col]. split; trivial; split. apply perp_per_1, perp_left_comm, perp_col with C0; trivial. apply le3456_lt__lt with P Q'. split. apply bet__le1213; trivial. intro; assert (Q = Q'); [|treat_equalities; auto]. apply between_cong with P; assumption. apply le_transitivity with B0 E; trivial. apply le_right_comm. apply t22_24_aux with A B0 C0; trivial. apply archi__obtuse_case_elimination; assumption. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad