proposition: Lemma cong_adae: cong a' d' a' e'.
proof: Proof. rewrite congP_aux /sqr_L2_norm_3D /a' /d' /e' !mxE /= ?add0r ?subr0 ?sqrrN //. 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