proposition: Lemma t22_7__cong : forall A B C D P Q, Saccheri A B C D -> Bet B P C -> Bet A Q D -> A <> Q -> Per P Q A -> Per A B C -> Cong P Q A B.
proof: Proof. intros A B C D P Q HSac HP HQ HAQ HPerQ HPer. assert(Hdiff := sac_distincts A B C D HSac). spliter. destruct (cong_dec P Q A B); auto. exfalso. apply (nlta A B C). elim(le_cases P Q A B). - intro. apply acute_per__lta; auto. apply (t22_7__acute _ _ _ D P Q); auto. split; auto. - intro. apply obtuse_per__lta; auto. apply (t22_7__obtuse _ _ _ D P Q); auto. split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma