proposition: Lemma inner_pasch : inner_paschP Point bet'.
proof: Proof. move=> a b c p q Hb1 Hb2 ? ? ? ? HNC. destruct (@inner_pasch _ _ a b c p q) as [x [Hb3 Hb4]]; rewrite -?bet_betS //. by exists x; rewrite /bet'. 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) mathcomp(zmodp) mathcomp(tuple fintype bigop) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence