proposition: Lemma archi__gradaexp_destruction : archimedes_axiom -> forall A B C, ~ Col A B C -> exists P Q R, GradAExp A B C P Q R /\ Obtuse P Q R.
proof: Proof. intros archi A B C HNCol. destruct (archi__grada_destruction archi A B C HNCol) as [D [E [F [HGA HNIsi]]]]. destruct (gradaexp_destruction_aux A B C D E F HGA) as [P [Q [R [HGAE HUn]]]]. exists P; exists Q; exists R; split; trivial. destruct HUn as [HObtuse|HLea]; trivial. assert_diffs. apply nsams__obtuse; auto. intro HIsi; apply HNIsi. apply sams_lea2__sams with P Q R P Q R; trivial. apply grada__lea, gradaexp__grada, HGAE. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel