proposition: Lemma obtuse_sac__oah : forall A B C D, Saccheri A B C D -> Obtuse A B C -> hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. intros A B C D HSac HPer A' B' C' D' HSac'. assert(Hdiff := sac_distincts A B C D HSac). assert(Hdiff' := sac_distincts A' B' C' D' HSac'). spliter. elim(angle_partition A' B' C'); auto. { intro Hacute'. exfalso. apply (nlta A B C). apply (acute_obtuse__lta); auto. assert(aah := acute_sac__aah A' B' C' D' HSac' Hacute'). apply (aah _ _ _ D); auto. } intro HUn. destruct HUn as [HPer'|]; auto. exfalso. apply (nlta A B C). apply (obtuse_per__lta); auto. assert(rah := per_sac__rah A' B' C' D' HSac' HPer'). apply (rah _ _ _ D); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma