proposition: Lemma X_in_disk (a b p q : Point) : (exists X' : 'rV[R]_n.+1, bet (# p) X' (# b) /\ bet (# q) X' (# a))-> (exists X : Point, bet (# p) (# X) (# b) /\ bet (# q) (# X) (# a)).
proof: Proof. move => H. destruct H. assert ((x *m x^T) 0 0 < 1). apply bet_in_disk with (#p) (#b). by destruct p. by destruct b. destruct H as [H _] ; assumption. exists (exist (fun p => (p *m p^T) 0 0 < 1) x H0). exact: H. 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