proposition: Lemma congP_aux a b c d : cong a b c d = (sqr_L2_norm_3D a b == sqr_L2_norm_3D c d).
proof: Proof. rewrite /cong !congP_aux' /sqr_L2_norm_3D; apply /eqP/eqP=> [|->] //. move=>/matrixP /(_ 0 0) /eqP; rewrite !mxE /= !mulr1n; apply /eqP. 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