proposition: Lemma mx11_eq (a b : 'rV[R]_1): a == b = (a 0 0 == b 0 0).
proof: Proof. apply /eqP/eqP=> [-> //|H]. by apply/matrixP=> i j; rewrite !ord1. 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