proposition: Lemma not_oah : hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals -> ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. intros HUn oah. destruct ex_saccheri as [A [B [C [D HSac]]]]. assert(Hdiff := sac_distincts A B C D HSac). spliter. apply (nlta A B C). assert(Obtuse A B C) by (apply (oah _ _ _ D); auto). destruct HUn as [aah|rah]. - apply (acute_obtuse__lta); auto. apply (aah _ _ _ D); auto. - apply (obtuse_per__lta); auto. apply (rah _ _ _ D); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma