proposition: Lemma lt_sac__obtuse : forall A B C D, Saccheri A B C D -> Lt B C A D <-> Obtuse A B C.
proof: Proof. intros A B C D HSac. assert(HM := midpoint_existence B C). destruct HM as [M HM]. assert(HN := midpoint_existence A D). destruct HN as [N HN]. assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN). assert (HCongA : CongA A B C M B A). { apply sac_distincts in HSac; spliter. assert_diffs. apply conga_right_comm, out2__conga. apply out_trivial; auto. apply bet_out; Between. } split. - intro HLt. apply (conga_obtuse__obtuse M B A); CongA. apply (lam_lt__obtuse N); trivial. apply lt_comm, lt_mid2__lt12 with C D; trivial. - intro HObtuse. apply lt_mid2__lt13 with M N; trivial. apply lt_comm, lam_obtuse__lt; trivial. apply (conga_obtuse__obtuse A B C); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma