proposition: Lemma angles_archi_aux1 : archimedes_axiom -> forall A B C D E F, ~ Col A B C -> ~ Bet D E F -> exists P Q R, GradA A B C P Q R /\ (LeA D E F P Q R \/ ~ SAMS P Q R A B C).
proof: Proof. intros archi A B C D E F HNCol HNBet. assert (Hdiff : D <> E /\ F <> E) by (split; intro; subst E; Between); spliter. assert_diffs. destruct (angle_bisector D E F) as [F1 [HInangle HConga]]; auto. assert(HNOS : ~ OS E F1 D F). { assert_diffs. elim (col_dec D E F1). intros HCol; apply col123__nos; Col. intro HNCol1. apply l9_9, invert_two_sides, in_angle_two_sides; Col. apply not_col_permutation_1, (ncol_conga_ncol D E F1); CongA. } assert (HSuma : SumA D E F1 D E F1 D E F) by (assert_diffs; exists F; repeat (split; CongA); Cop). destruct (archi_in_acute_angles archi A B C D E F1) as [P1 [Q1 [R1 [HGA HLea]]]]; trivial. { apply nbet_sams_suma__acute with D E F; trivial. assert_diffs; split; trivial; split. right; intro HBet; apply HNBet, bet_in_angle_bet with F1; trivial. exists F; repeat (split; CongA); Cop. elim (col_dec D E F1). intros HCol HTS; destruct HTS; Col. intro HNCol1. elim (col_dec D E F). intros HCol HTS; destruct HTS as [_ []]; Col. intro HNCol2; apply l9_9_bis, in_angle_one_side; Col. } assert_diffs. destruct (sams_dec P1 Q1 R1 P1 Q1 R1) as [HIsi|HNIsi]. { destruct (ex_suma P1 Q1 R1 P1 Q1 R1) as [P [Q [R HSuma1]]]; auto. exists P; exists Q; exists R; split. apply grada2_sams_suma__grada with P1 Q1 R1 P1 Q1 R1; trivial. left; apply sams_lea2_suma2__lea with D E F1 D E F1 P1 Q1 R1 P1 Q1 R1; trivial. } destruct (angles_archi_aux A B C P1 Q1 R1 P1 Q1 R1) as [P [Q [R [HGA1 HNsams1]]]]; trivial. exists P; exists Q; exists R; split; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel