proposition: Lemma acute_archi_aux2 : forall O A0 A1 B C, Per O A0 B -> O <> A0 -> B <> A0 -> Bet A0 A1 B -> A0 <> A1 -> Grad A0 A1 C -> exists P, exists Q, exists R, GradA A0 O A1 P Q R /\ (LeA A0 O B P Q R \/ exists A', Bet A0 A1 A' /\ Bet A0 A' B /\ CongA P Q R A0 O A' /\ Le A0 C A0 A' /\ exists A, Bet A0 A A' /\ CongA A O A' A0 O A1 /\ Le A0 A1 A A').
proof: Proof. intros O A0 A1 B E HPer HOA0 HBA0 HBet HA0A1 HG. assert (HNCol : ~ Col O A0 B) by (apply per_not_col; auto). assert (HNCol1 : ~ Col A0 O A1) by (intro; apply HNCol; ColR). assert_diffs. induction HG; rename A into A0; rename B0 into A1. exists A0; exists O; exists A1; split; [apply grada_init; CongA|]. right; exists A1; repeat (split; CongA); Between; Le. exists A0; repeat (split; CongA); Between; Le. destruct IHHG as [P [Q [R [HGA HUn]]]]; auto. destruct HUn as [HLea|HA']. exists P; exists Q; exists R; split; trivial; left; trivial. destruct HA' as [A' [HBet1' [HBet2' [HConga' [HLe' HA]]]]]. destruct HA as [A [HBet1 [HConga HLe]]]. assert (HIsi : SAMS P Q R A0 O A1). { apply sams_lea2__sams with A0 O B A0 O B. - apply acute__sams, l11_43_aux; Col. - apply (l11_30 A0 O A' A0 O B); CongA. exists A'; assert_diffs; split; CongA. repeat split; auto. exists A'; split; trivial. right; apply out_trivial; auto. - exists A1; split; CongA. repeat split; auto. exists A1; split; trivial. right; apply out_trivial; auto. } assert_diffs. destruct (ex_suma P Q R A0 O A1) as [P' [Q' [R' HSuma]]]; auto. assert (HGA' : GradA A0 O A1 P' Q' R') by (apply grada_stab with P Q R; trivial). exists P'; exists Q'; exists R'; split; trivial. destruct (acute_archi_aux1 O A0 A1 B P' Q' R') as [HLea|HA'']; auto. right; destruct HA'' as [A'' [HBet1'' [HBet2'' HConga'']]]. assert (HNCol2 : ~ Col A O A') by (apply (ncol_conga_ncol A0 O A1); Col; CongA). assert (HNCol3 : ~ Col A0 O A') by (intro; assert_diffs; apply HNCol; ColR). assert (HNCol4 : ~ Col A' O A''). { intro HCol; apply HNCol1. elim (eq_dec_points A' A''); intro; [|ColR]. treat_equalities. assert (HSuma2 : SumA A0 O A' A0 O A1 A0 O A'). apply (conga3_suma__suma P Q R A0 O A1 P' Q' R'); CongA. apply sams_suma__out546 in HSuma2; Col. apply (conga2_sams__sams P Q R A0 O A1); CongA. } assert (HNCol5 : ~ Col A0 O A'') by (intro; assert_diffs; apply HNCol4; ColR). assert (HBet4 : Bet A0 A' A''). { apply col_two_sides_bet with O. ColR. apply in_angle_two_sides; Col. apply lea_in_angle. apply (l11_30 P Q R P' Q' R'); CongA; apply sams_suma__lea123789 with A0 O A1; trivial. apply out_one_side; Col; apply l6_7 with B; [|apply l6_6]; assert_diffs; apply bet_out; auto. } assert (HConga4 : CongA A O A' A' O A''). { assert_diffs. assert (HNOS : ~ OS O A' A0 A'') by (apply l9_9; repeat split; auto; Col; exists A'; Col). apply conga_trans with A0 O A1; trivial. apply sams2_suma2__conga456 with P Q R P' Q' R'; trivial. - apply (conga2_sams__sams A0 O A' A' O A''); CongA. split; auto; split. right; intro; Col. exists A''; repeat (split; CongA); Cop. apply l9_9_bis, out_one_side; Col. apply bet_out; auto. - apply (conga3_suma__suma A0 O A' A' O A'' A0 O A''); CongA. exists A''; repeat (split; CongA); Cop. } assert (HLe'' : Le A0 A1 A' A''). apply le_transitivity with A A'; trivial; assert_diffs. apply lt__le, acute_archi_aux with O A0 B; eBetween. exists A''; repeat (split; trivial). apply bet2_le2__le1346 with C A'; auto. apply (l5_6 A0 A1 A' A''); Cong. exists A'; split; trivial; split; trivial. apply conga_trans with A O A'; CongA. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel