proposition: Lemma onemx_neq0 : @const_mx (Num.RealField.sort R) (S O) (S n) 0 != @const_mx (Num.RealField.sort R) (S O) (S n) 1.
proof: Proof. by apply/eqP=> /matrixP/(_ 0 0)/eqP; rewrite /const_mx !mxE eq_sym oner_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) mathcomp(tuple fintype bigop) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence