proposition: Lemma t22_17__aah : forall A B C M, ~ Col A B C -> Midpoint M A B -> Cong M A M C -> (Acute A C B <-> hypothesis_of_acute_saccheri_quadrilaterals).
proof: Proof. intros A B C M HNCol HM HCong. assert_diffs. split; intro. - destruct (saccheri_s_three_hypotheses) as [|[|]]; auto; exfalso; apply (nlta A C B). apply (acute_per__lta); auto; rewrite (t22_17__rah _ _ _ M); auto. apply (acute_obtuse__lta); auto; rewrite (t22_17__oah _ _ _ M); auto. - destruct (angle_partition A C B) as [|[|]]; auto; absurd(hypothesis_of_acute_saccheri_quadrilaterals); auto; apply not_aah. left; apply (t22_17__rah A B C M); auto. right; apply (t22_17__oah A B C M); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma