proposition: Lemma upper_dim : upper_dimP Point bet' cong'.
proof: Proof. move => a b c p q /eqP neq_pq _ _ _; move: neq_pq. rewrite /cong' !cong_abac_1D !neq_mx -subr_eq0 vector2_neq0 !mxE /= !subr_eq0. case: (p 0 0 =P q 0 0) => /= _; [case: (p 0 1 =P q 0 1) => //= _ | ] => _. rewrite /Col /bet'=> /eqP-> /eqP-> /eqP->; rewrite !bet_xxa !andbT; apply col_1D. rewrite /Col /bet'=> /andP[/eqP-> _] /andP[/eqP-> _] /andP[/eqP-> _]. rewrite !bet_xxa /=; apply col_1D. 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