proposition: Lemma row3_eq (a b c d e f : R) : row3 a b c == row3 d e f = [&& (a == d), (b == e) & (c == f)].
proof: Proof. apply /eqP; case: (a =P d)=> [->|/eqP Hv0]; case: (b =P e)=> [->|/eqP Hv1]; case: (c =P f)=> [->|/eqP Hv2] //; apply /eqP; rewrite eq3 !mxE ?eqxx //= andbC //; rewrite ?negb_and ?negb_and3 ?Hv0 ?Hv1 ?Hv2 //. 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