proposition: Lemma existential_triangle__rah : postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights -> postulate_of_right_saccheri_quadrilaterals.
proof: Proof. intro et. destruct et as [A [B [C [D [E [F]]]]]]. spliter. apply (t22_14__rah A B C D E F); auto. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Annexes.saccheri