proposition: Lemma t22_9__obtuse : forall N M P Q R S, Lambert N M P Q -> Lambert N M R S -> Bet M P R -> Bet N Q S -> (Obtuse S R M <-> Obtuse Q P M).
proof: Proof. intros N M P Q R S HLamP HLamR HR HS. destruct (t22_9_aux N M P Q R S HLamP HLamR HR HS) as [[][]]. unfold Lambert in HLamP. unfold Lambert in HLamR. spliter. split; intro. - destruct(angle_partition Q P M) as [|[|]]; auto; exfalso; apply (nlta S R M). apply acute_obtuse__lta; auto. apply obtuse_per__lta; auto. - destruct(angle_partition S R M) as [|[|]]; auto; exfalso; apply (nlta Q P M). apply acute_obtuse__lta; auto. apply obtuse_per__lta; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma