proposition: Lemma gradaexp_destruction_aux : forall A B C P Q R, GradA A B C P Q R -> exists S T U, GradAExp A B C S T U /\ (Obtuse S T U \/ LeA P Q R S T U).
proof: Proof. intros A B C. induction 1. assert_diffs; exists D; exists E; exists F; split; [apply gradaexp_init|right]; Lea. destruct IHGradA as [P [Q [R [HGAE HUn]]]]. assert (Hd := HGAE); apply gradaexp__grada, grada_distincts in Hd; spliter. destruct (sams_dec P Q R P Q R) as [HIsi|HNIsi]. { destruct HUn as [Habs|HLea]. absurd (SAMS P Q R P Q R); trivial; apply obtuse__nsams, Habs. destruct (ex_suma P Q R P Q R) as [S [T [U HSuma]]]; auto. exists S; exists T; exists U; split. apply gradaexp_stab with P Q R; trivial. right; apply sams_lea2_suma2__lea with D E F A B C P Q R P Q R; trivial. apply grada__lea, gradaexp__grada, HGAE. } apply nsams__obtuse in HNIsi; auto. 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