proposition: Lemma t22_7__lt1256 : forall A B C D P Q, Saccheri A B C D -> Bet B P C -> Bet A Q D -> A <> Q -> Q <> D -> Per P Q A -> Obtuse A B C -> Lt A B P Q.
proof: Proof. intros A B C D P Q HSac HP HQ HAQ HQD HPerQ Hobtuse. assert(Hdiff := sac_distincts A B C D HSac). spliter. destruct(cong_dec P Q A B). { exfalso. apply (nlta A B C). apply obtuse_per__lta; auto. apply (t22_7__per _ _ _ D P Q); auto. } split; Cong. destruct(le_cases P Q A B); auto. exfalso. apply (nlta A B C). apply acute_obtuse__lta; auto. apply (t22_7__acute _ _ _ D P Q); auto. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma