proposition: Lemma t22_8__cong : 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 -> Per A B C -> Cong R S A B.
proof: Proof. intros A B C D R S HSac. intros. elim(cong_dec R S A B); auto. intro. assert(Hdiff := sac_distincts A B C D HSac). spliter. exfalso. apply (nlta A B C). destruct(le_cases R S A B). - apply obtuse_per__lta; auto. apply (t22_8__obtuse _ _ _ D R S); auto. split; auto. - apply acute_per__lta; auto. apply (t22_8__acute _ _ _ D R S); auto. split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma