proposition: Lemma acute_archi_aux : forall O A B C D E, Per O A B -> O <> A -> B <> A -> C <> D -> D <> E -> Bet A C D -> Bet C D E -> Bet D E B -> CongA C O D D O E -> Lt C D D E.
proof: Proof. intros O A B C D E HPer HOA HBA HCD HDE HBet1 HBet2 HBet3 HCongA. assert_diffs. assert (HNCol1 : ~ Col O A B) by (apply per_not_col; auto). assert (HNCol2 : ~ Col O A D). assert_cols; intro; elim (eq_dec_points A C); intro; [treat_equalities|]; apply HNCol1; ColR. destruct (angle_construction_1 A D O O D E) as [P [HP1 HP2]]; Col. intro; apply HNCol2; ColR. assert (HAcute : Acute A D O). apply l11_43_aux; Col; left; apply l8_2, per_col with B; auto; ColR. assert (HF : InAngle P O D E). { apply lea_in_angle; Side. apply (l11_30 A D O E D O); CongA. destruct (acute_chara A D O E) as [HD HI]; eBetween. apply lta__lea, HD, HAcute. } destruct HF as [_ [_ [HDP [F [HBet4 [Heq|HOut]]]]]]. exfalso; subst F; apply HNCol2; ColR. assert_diffs. assert (HCongA1 : CongA A D O O D F). apply (l11_10 A D O O D P); try apply out_trivial; auto. assert (HCongA2 : CongA O D C A D O). apply conga_left_comm, out2__conga; [apply l6_6, bet_out|apply out_trivial]; Between. clear dependent P. assert (HNCol3 : ~ Col O D F) by (apply (ncol_conga_ncol A D O); Col). assert_diffs. destruct (l11_50_1 O D C O D F) as [HCong1 [HCong2 HCongA3]]; Cong. intro; apply HNCol2; ColR. apply (l11_10 D O C D O E); CongA; try (apply out_trivial; auto); apply bet_out; auto. apply conga_trans with A D O; trivial. apply (cong2_lt__lt D F D E); Cong. assert (HNCol4 : ~ Col E D F). { intro; elim (eq_dec_points E F); intro; [|apply HNCol3; ColR]. treat_equalities. apply (acute_not_per A D O); trivial. apply l8_2, per_col with C; Col. exists E; repeat split; Cong. } assert_diffs. apply l11_44_2_b; trivial. apply lta_trans with F D O. - destruct (l11_41 D E O C) as [Hlta1 Hlta2]; Between. intro; apply HNCol3; ColR. apply (conga_preserves_lta D E O O D C); trivial; [apply out2__conga|apply (l11_10 O D A F D O)]; CongA; try (apply out_trivial; auto); apply bet_out; Between. - destruct (l11_41 F O D E); Col. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel