proposition: Lemma cong_pseudo_reflexivity : ~ cong_pseudo_reflexivityP Point cong'.
proof: Proof. move=> HF; move: onemx_neq0 (HF (const_mx 0) (const_mx 1)). by rewrite /cong'; case: (const_mx 0 =P const_mx 1). 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