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

Section rectangle_principle_rectangle_existence.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma rectangle_principle__rectangle_existence : postulate_of_right_lambert_quadrilaterals -> postulate_of_existence_of_a_right_lambert_quadrilateral.
Proof.
(* Goal: forall _ : @postulate_of_right_lambert_quadrilaterals Tn, @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  intros rectangle.
(* Goal: @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  destruct ex_saccheri as [A [B [C [D HSac]]]].
(* Goal: @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  destruct (midpoint_existence B C) as [M HM].
(* Goal: @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  destruct (midpoint_existence A D) as [N HN].
(* Goal: @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN).
(* Goal: @postulate_of_existence_of_a_right_lambert_quadrilateral Tn *)
  exists N; exists M; exists B; exists A.
(* Goal: and (@Lambert Tn N M B A) (@Per Tn M B A) *)
  split.
(* Goal: @Lambert Tn N M B A *)
(* Goal: @Per Tn M B A *)
    assumption.
(* Goal: @Lambert Tn N M B A *)
(* Goal: @Per Tn M B A *)
    apply (rectangle N); assumption.
Qed.

End rectangle_principle_rectangle_existence.