proposition: Lemma neq_mx10 (n : nat) : ((1%:M : 'M[R]_n.+1) == 0) = false.
proof: Proof. apply /eqP. intro H. move: (@matrix_nonzero1 R n). by rewrite H eqxx. 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