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