proposition: Lemma acute_archi_aux1 : forall O A0 A1 B P Q R, Per O A0 B -> B <> A0 -> Bet A0 A1 B -> GradA A0 O A1 P Q R -> A0 <> A1 -> LeA A0 O B P Q R \/ exists A, Bet A0 A1 A /\ Bet A0 A B /\ CongA P Q R A0 O A.
proof: Proof. intros O A0 A1 B P Q R HPer HBA0 HBet HGA HA0A1. assert (Hdiff := grada_distincts A0 O A1 P Q R HGA); spliter. assert (HNCol : ~ Col O A0 B) by (apply per_not_col; auto). assert_diffs. elim (lea_total A0 O B P Q R); auto. intro HLeA; right. assert (HNCol2 : ~ Col P Q R). { intro HCol. assert (HBet1 : Bet P Q R). apply not_out_bet; trivial. intro HOut; assert (Out O A0 A1) by (apply grada_out__out with P Q R; trivial). apply HNCol; ColR. assert (Bet A0 O B) by (apply bet_lea__bet with P Q R; trivial). apply HNCol; Col. } destruct (angle_construction_1 P Q R A0 O B) as [C [Hconga HOS]]; Col. assert (HA : InAngle C A0 O B). apply lea_in_angle; Side; apply (l11_30 P Q R A0 O B); CongA. destruct HA as [_ [_ [HCO [A [HA HUn]]]]]. destruct HUn as [Heq|Hout]. exfalso; treat_equalities; apply HNCol; Col. exists A. assert (Hconga1 : CongA P Q R A0 O A). apply l11_10 with P R A0 C; trivial; apply out_trivial; auto. repeat (split; trivial). elim (eq_dec_points A1 A). intro; subst A; Between. intro HAA1. apply (ncol_conga_ncol P Q R A0 O A) in HNCol2; trivial. assert (HInangle : InAngle A1 A0 O A). { apply lea_in_angle. apply (l11_30 A0 O A1 P Q R); CongA; apply grada__lea; trivial. apply out_one_side; auto. assert_diffs. apply l6_7 with B; [|apply l6_6]; apply bet_out; auto. } destruct HInangle as [_ [_ [_ [X [HX1 HUn]]]]]. destruct HUn as [HX2|HX2]. subst X; exfalso; Col. elim (eq_dec_points X A1); intro. subst X; trivial. exfalso; apply HNCol2; ColR. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel