proposition: Lemma t22_8__lt5612 : forall A B C D R S, Saccheri A B C D -> Bet B C R -> Bet A D S -> D <> S -> Per A S R -> Obtuse A B C -> Lt R S A B.
proof: Proof. intros A B C D R S HSac. intros. assert_diffs. destruct(cong_dec R S A B). { exfalso. apply (nlta A B C). apply obtuse_per__lta; auto. apply (t22_8__per _ _ _ D R S); auto. } destruct(le_cases R S A B). split; auto. exfalso. apply (nlta A B C). apply acute_obtuse__lta; auto. apply (t22_8__acute _ _ _ D R S); auto. split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma