proposition: Lemma angles_archi_aux : forall A B C D E F G H I, GradA A B C D E F -> GradA A B C G H I -> ~ SAMS D E F G H I -> exists P Q R, GradA A B C P Q R /\ ~ SAMS P Q R A B C.
proof: Proof. intros A B C D E F G H I HGA1 HGA2. induction HGA2. intro HNIsi; exists D; exists E; exists F; split; trivial. assert (Hd := grada_distincts A B C D E F HGA1); spliter. intro HIsi; apply HNIsi, (conga2_sams__sams D E F A B C); CongA. intro HNIsi. elim (sams_dec D E F D0 E0 F0); [|apply IHHGA2; trivial]. intro HIsi; clear IHHGA2. assert (Hd := sams_distincts D E F D0 E0 F0 HIsi); spliter. destruct (ex_suma D E F D0 E0 F0) as [P [Q [R HSuma]]]; auto. exists P; exists Q; exists R; split. apply grada2_sams_suma__grada with D E F D0 E0 F0; trivial. intro HIsi2; apply HNIsi, sams_assoc_1 with D0 E0 F0 A B C P Q R; trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel