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

Section triangle_existential_triangle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma triangle__existential_triangle : triangle_postulate -> postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights.
Proof.
(* Goal: forall _ : @triangle_postulate Tn, @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  intro triangle.
(* Goal: @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  destruct lower_dim_ex as [A [B [C]]].
(* Goal: @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  assert(~ Col A B C) by (unfold Col; assumption).
(* Goal: @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  assert_diffs.
(* Goal: @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  destruct (ex_trisuma A B C) as [D [E [F]]]; auto.
(* Goal: @postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights Tn *)
  exists A; exists B; exists C; exists D; exists E; exists F.
(* Goal: and (not (@Col Tn A B C)) (and (@TriSumA Tn A B C D E F) (@Bet Tn D E F)) *)
  repeat split.
(* Goal: @TriSumA Tn A B C D E F *)
(* Goal: @Bet Tn D E F *)
    assumption.
(* Goal: @TriSumA Tn A B C D E F *)
(* Goal: @Bet Tn D E F *)
    assumption.
(* Goal: @TriSumA Tn A B C D E F *)
(* Goal: @Bet Tn D E F *)
    apply (triangle A B C); assumption.
Qed.

End triangle_existential_triangle.