proposition: Lemma t22_17__oah : forall A B C M, ~ Col A B C -> Midpoint M A B -> Cong M A M C -> (Obtuse A C B <-> hypothesis_of_obtuse_saccheri_quadrilaterals).
proof: Proof. intros A B C M HNCol HM HCong. assert_diffs. assert(SumA C A B A B C A C B) by (apply (cong_mid__suma _ _ _ M); auto). assert(HSuma := ex_suma A C B B C A). destruct HSuma as [P [Q [R]]]; auto. split; intro HO. - apply (t22_14__oah A B C B C A); Col; SumA. apply obtuse__nsams; apply obtuse_sym; auto. - apply obtuse_sym. apply nsams__obtuse; auto. apply (t22_14__nsams HO A B C); Col; SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma