Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.

Section existential_saccheri_rah.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma existential_saccheri__rah : postulate_of_existence_of_a_right_saccheri_quadrilateral -> postulate_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @postulate_of_existence_of_a_right_saccheri_quadrilateral Tn, @postulate_of_right_saccheri_quadrilaterals Tn *)
  intro HABCD.
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  destruct HABCD as [A [B [C [D [HSac HPer]]]]].
(* Goal: @postulate_of_right_saccheri_quadrilaterals Tn *)
  apply (per_sac__rah A B C D HSac HPer).
Qed.

End existential_saccheri_rah.
