proposition: Lemma congP a b c d : reflect ((sqr_L2_norm_1D_i a b 0 == sqr_L2_norm_1D_i c d 0) /\ (sqr_L2_norm_1D_i a b 1 == sqr_L2_norm_1D_i c d 1)) (cong' a b c d).
proof: Proof. by rewrite !congP_aux; exact /andP. 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