proposition: Lemma cong_identity : cong_identityP Point cong'.
proof: Proof. move => a b c /congP[H0 H1]; apply /eqP; rewrite vector2_eq; move: H0 H1. rewrite /sqr_L2_norm_1D_i /sqr_L2_norm_1D !mxE eqxx !subrr !mulr1n expr0n. by rewrite !sqrf_eq0 !subr_eq0=> /eqP -> /eqP ->; rewrite !eqxx. 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