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

Section rah_triangle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma rah__triangle : postulate_of_right_saccheri_quadrilaterals -> triangle_postulate.
Proof.
(* Goal: forall _ : @postulate_of_right_saccheri_quadrilaterals Tn, @triangle_postulate Tn *)
  intros rah A B C D E F.
(* Goal: forall _ : @TriSumA Tn A B C D E F, @Bet Tn D E F *)
  apply (t22_14__bet rah).
Qed.

End rah_triangle.