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