proposition: Lemma lower_dim : lower_dimP Point (@bet R 3) a' b' c'.
proof: Proof. unfold lower_dimP. move=> H. move: H. rewrite /Col /bet /betE. rewrite ab_neq bc_neq ca_neq /=. rewrite /betS. rewrite betR_abc. rewrite betR_bca. elim (betR_cab)=> [->|->]; 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.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence