proposition: Lemma eq3 (a b : Point) : a == b = ((a 0 0 == b 0 0) && ((a 0 1 == b 0 1) && (a 0 2%:R == b 0 2%:R))).
proof: Proof. apply /eqP/and3P=> [->|[/eqP eq0 /eqP eq1 /eqP eq2]] ; rewrite ?eqxx //. apply/rowP=> j; case: j => [] [|[| []] //] //= p. rewrite (@ord_inj _ (Ordinal p) 0) //. rewrite (@ord_inj _ (Ordinal p) 1) //. rewrite (@ord_inj _ (Ordinal p) 2%:R) //. 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