proposition: Lemma archi__grada_destruction : archimedes_axiom -> forall A B C, ~ Col A B C -> exists P Q R, GradA A B C P Q R /\ ~ SAMS P Q R A B C.
proof: Proof. intros archi A B C HNCol. destruct (segment_construction A B A B) as [A0 [HBet HCong]]. assert_diffs. destruct (archi_in_angles archi A B C A B A0) as [P [Q [R [HGA HUn]]]]; auto. exists P; exists Q; exists R; split; auto. destruct HUn as [HLea|]; trivial. intro HIsi. destruct HIsi as [_ [[HOut|HNBet] _]]. apply HNCol; Col. apply HNBet, (bet_lea__bet A B A0); trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel