proposition: Lemma archi_in_acute_angles : archimedes_axiom -> forall A B C D E F, ~ Col A B C -> Acute D E F -> exists P Q R, GradA A B C P Q R /\ LeA D E F P Q R.
proof: Proof. intros archi A B C D E F HNCol HAcute. assert_diffs. elim (col_dec D E F). { intro HCol; exists A; exists B; exists C; split. apply grada_init; CongA. apply l11_31_1; auto; apply not_bet_out; trivial. intro HBet; apply (nlta D E F), acute_obtuse__lta; trivial. apply bet__obtuse; auto. } intro HNCol1. elim (lea_total D E F A B C); auto; intro HLea. exists A; exists B; exists C; split; trivial; apply grada_init; CongA. destruct (l8_18_existence D E F) as [D0 [HD0 HD0']]; trivial. assert (HOut : Out E D0 D) by (apply acute_col_perp__out with F; Col; Perp; apply acute_sym; trivial). assert_diffs. assert (HConga : CongA D E F D0 E F) by (apply out2__conga; [|apply out_trivial]; auto). apply (acute_conga__acute D E F D0 E F) in HAcute; trivial. apply (l11_30 A B C D E F A B C D0 E F) in HLea; CongA. apply (ncol_conga_ncol D E F D0 E F) in HNCol1; trivial. assert (HPer : Per E D0 F) by (apply perp_per_1, perp_left_comm, perp_col with D; Perp; Col). clear H0 HD0 HD0' HOut H9. destruct (angle_construction_1 A B C D0 E F) as [D1' [HConga1 HOS]]; trivial. destruct (lea_in_angle D0 E F D1') as [_ [_ [_ [D1 [HBet HUn]]]]]; Side. apply (l11_30 A B C D0 E F); CongA. destruct HUn as [Heq|HOut]. exfalso; subst D1; Col. assert (HConga2 : CongA A B C D0 E D1). apply (l11_10 A B C D0 E D1'); trivial; apply out_trivial; auto. apply one_side_not_col123 in HOS. assert_diffs. assert (D0 <> D1) by (intro; subst D1; apply HOS; Col). clear dependent D1'. destruct (segment_construction D0 F D0 F) as [F' [HF'1 HF'2]]. destruct (archi D0 D1 D0 F') as [G [HG1 HG2]]; auto. destruct (acute_archi_aux2 E D0 D1 F G) as [P [Q [R [HGA HUn]]]]; auto. exists P; exists Q; exists R; split. assert (Hdistincts := grada_distincts D0 E D1 P Q R HGA); spliter. apply (conga2_grada__grada D0 E D1 P Q R); CongA. destruct HUn as [HLea2|Habs]. assert_diffs; apply (l11_30 D0 E F P Q R); CongA. exfalso. destruct Habs as [A' [HBet2 [HBet3 [HConga3 [HLe HA]]]]]. apply (le__nlt D0 F' D0 G); trivial. apply le1234_lt__lt with D0 F. apply le_transitivity with D0 A'; Le. split; Le. intro HCong. assert (F = F') by (apply between_cong with D0; trivial). treat_equalities; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel