proposition: Lemma inner_pasch : inner_paschP Point bet'.
proof: Proof. rewrite /bet' => a b c p q bet_apc ? /eqP n1 /eqP n2 /eqP n3 /eqP n4 NC. rewrite !point_vector_neq in n1, n2, n3, n4. apply X_in_disk. by apply (inner_pasch_vector bet_apc)=> //; apply /eqP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence