proposition: Lemma t22_17__rah : forall A B C M, ~ Col A B C -> Midpoint M A B -> Cong M A M C -> (Per A C B <-> hypothesis_of_right_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 HR. - apply (t22_14__rah C A B P Q R); Col. exists A; exists C; exists B; auto. apply (per2_suma__bet A C B B C A); Perp. - apply (bet_suma__per _ _ _ P Q R); SumA. apply (t22_14__bet HR C A B). exists A, C, B; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma