proposition: Lemma lower_dim : lower_dimP Point bet' a' b' c'.
proof: Proof. move=> H; move: H; rewrite /Col /bet' /bet /betE ab_neq bc_neq ca_neq. rewrite /betS betR_abc betR_bca; elim (@betR_cab R 0)=> [->|->]; by rewrite !ltxx ltr01 /= ![_ && false]andbC /=; firstorder. 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) GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence