proposition: Lemma inner_pasch_gen a b c p q : bet a p c -> bet b q c -> exists x, bet p x b /\ bet q x a.
proof: Proof. case: (a =P p)=> [->|?]; first by exists p; rewrite bet_xxa bet_axx. case: (p =P c)=> [->|?]; first by exists q; rewrite bet_xxa bet_sym. case: (b =P q)=> [->|?]; first by exists q; rewrite bet_xxa bet_axx. case: (q =P c)=> [->|?]; first by exists p; rewrite bet_xxa bet_sym. have: ( (bet a b c \/ bet b c a \/ bet c a b) \/ ~ (bet a b c \/ bet b c a \/ bet c a b)). by case: (bet a b c); case: (bet b c a); case: (bet c a b); intuition. suff: (forall a b c p q, bet a b c -> a <> p -> p <> c -> b <> q -> q <> c -> bet a p c -> bet b q c -> exists x, bet p x b /\ bet q x a). move=> H [[?|[?|?]]|?] ? ?; [..|by apply inner_pasch with c]; [apply (H a b c p q)|exists c|destruct (H b a c q p) as [x []]]=> //; [split| |by exists x; split]; rewrite bet_sym //; [apply bet_inner_transitivity with a|apply bet_inner_transitivity with b]; by rewrite // bet_sym. clear dependent p; clear dependent q; clear a b c=> a b c p q Hb1 Hc1 Hc2. rewrite bet_betS //; clear Hc1 Hc2 => Hc1 Hc2 Hb2; rewrite bet_betS //. clear Hc1 Hc2; move: Hb1 Hb2; case: (a =P q)=> [-> ? Hb1 Hb2|?]. exists q; rewrite bet_axx; split; rewrite // bet_sym. by apply bet_inner_transitivity with c; rewrite /bet ?Hb1 ?Hb2 orbT. case: (b =P p)=> [-> ? ? Hb|? _ ? ?]; last by destruct (@inner_pasch'' a b c p q) as [x [Hb1 Hb2]]; [..|exists x; split]; rewrite // /bet ?Hb1 ?Hb2 orbT. exists p; split; rewrite ?bet_axx // bet_sym. by apply bet_inner_transitivity with c; rewrite // /bet Hb orbT. 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