proposition: Lemma Euclid5 : forall a p q r s t, BetS r t s -> BetS p t q -> BetS r a q -> Cong p t q t -> Cong t r t s -> nCol p q s -> exists X, BetS p a X /\ BetS s q X.
proof: Proof. intros. assert (T:tarski_s_parallel_postulate -> euclid_5). { assert (T:=equivalent_postulates_without_decidability_of_intersection_of_lines_bis). unfold all_equiv.all_equiv in *. apply T;simpl;auto 10. } assert (T2:euclid_5). apply T. unfold tarski_s_parallel_postulate. apply euclid. unfold euclid_5 in *. assert (T3:exists I : Tpoint, Definitions.BetS s q I /\ Definitions.BetS p a I). apply (T2 p q r s t a); auto using BetS_BetS. unfold BetS in *;simpl in *; unfold Definitions.BetS in *;spliter;Between. intro HnCol. apply Col_Col in HnCol. apply nCol_not_Col in H4;intuition. Cong. destruct T3 as [X HX]. exists X;spliter;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates