proposition: Lemma inner_pasch' a b c p q (k1 := betR a p c) (k2 := betR b q c) : betS a p c -> betS b q c -> ~ (bet a b c \/ bet b c a \/ bet c a b) -> exists x, betS p x b /\ betS q x a.
proof: Proof. rewrite /bet; case: (b =P p) => [-> ->|bp_neq]; [rewrite orbT; intuition|]. case: (a =P q)=> [-> _|aq_neq ? ? _]. by rewrite [betS c q b]betS_sym=> ->; rewrite orbT; intuition. by destruct (@inner_pasch'' a b c p q) as [x []]=> //; exists x. 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