proposition: Lemma t22_11__obtuse : forall A B C D, Saccheri A B C D -> (LtA B D C A B D <-> Obtuse A B C).
proof: Proof. intros A B C D HSac. split. - intro. apply (lt_sac__obtuse _ _ _ D); auto. unfold Saccheri in HSac. spliter. apply lt_right_comm. apply (t18_18 B _ _ D); Cong. apply lta_left_comm; auto. - intro Hobtuse. apply <- (lt_sac__obtuse A B C D) in Hobtuse; trivial. assert(Hdiff := sac_distincts A B C D HSac). unfold Saccheri in HSac. spliter. apply lta_left_comm. apply t18_19; Cong. apply lt_right_comm; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma