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

Section rah_existential_saccheri.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma rah__existential_saccheri : postulate_of_right_saccheri_quadrilaterals -> postulate_of_existence_of_a_right_saccheri_quadrilateral.
Proof.
(* Goal: forall _ : @postulate_of_right_saccheri_quadrilaterals Tn, @postulate_of_existence_of_a_right_saccheri_quadrilateral Tn *)
  intro rah.
(* Goal: @postulate_of_existence_of_a_right_saccheri_quadrilateral Tn *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @postulate_of_existence_of_a_right_saccheri_quadrilateral Tn *)
  exists A; exists B; exists C; exists D.
(* Goal: and (@Saccheri Tn A B C D) (@Per Tn A B C) *)
  split.
(* Goal: @Saccheri Tn A B C D *)
(* Goal: @Per Tn A B C *)
    assumption.
(* Goal: @Per Tn A B C *)
    apply (rah A B C D HSac).
Qed.

End rah_existential_saccheri.