proposition: Lemma proclus a b c d p q : par a b c d -> col a b p -> ~ col a b q -> coplanar c d p q -> exists y, col p q y /\ col c d y.
proof: Proof. cut (proclus_postulate); [move => HP HPar HC HNC HCop|]; last first. have: tarski_s_parallel_postulate. by unfold tarski_s_parallel_postulate; apply euclidT. apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; tauto. destruct (HP a b c d p q) as [x []]; [..|exists x]; [|intuition..]. move: HPar => {HC HNC HCop} [HParS|]; [left|right; intuition]. move: HParS => [HCop HNI]; split; [intuition|]. by move => [x [? ?]]; apply HNI; exists x; intuition. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec