proposition: Lemma archi_in_angles : archimedes_axiom -> forall A B C D E F, ~ Col A B C -> D <> E -> F <> E -> 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 HDE HFE. elim (bet_dec D E F); [|apply angles_archi_aux1; trivial]. intro HBet1. destruct (segment_construction A B A B) as [A0 [HBet HCong]]. assert_diffs. assert (HNCol1 : ~ Col A0 B C) by (intro; apply HNCol; ColR). destruct (angles_archi_aux1 archi A B C C B A0) as [P1 [Q1 [R1 [HGA HUn]]]]; Between. intro; apply HNCol1; Col. elim (sams_dec P1 Q1 R1 A B C); [|intro; exists P1; exists Q1; exists R1; auto]. intro HIsi. destruct HUn as [HLea|HNIsi]; [|exfalso; auto]. assert_diffs. destruct (ex_suma P1 Q1 R1 A B C) as [P [Q [R HSuma]]]; auto. exists P; exists Q; exists R; split. apply grada_stab with P1 Q1 R1; trivial. suma.assert_diffs. left; apply l11_31_2; auto. apply (bet_lea__bet A B A0); trivial. apply sams_lea2_suma2__lea with A0 B C A B C P1 Q1 R1 A B C; Lea. exists A; repeat (split; CongA); Cop. apply l9_9; repeat split; auto. exists B; split; Col; Between. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel