proposition: Lemma upper_dim : upper_dimP (@Point 1 R) (@bet' 1 R) (@cong' 1 R).
proof: Proof. rewrite /cong' => a b c p q ? ? ? ? /eqP -> /eqP -> /eqP ->. by rewrite /Col /bet' bet_axx; left. 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