proposition: Lemma neq_mx (n : nat) (a b : R) : ((a%:M : 'M[R]_n.+1) == b%:M) = (a == b).
proof: Proof. by rewrite -scalemx1 -[b%:M]scalemx1 -subr_eq0 -scalerBl scalemx_eq0 neq_mx10 orbF subr_eq0. 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