proposition: Lemma cong_abac_1D (a b c : 'rV[R]_1) : (cong a b a c) = ((b == c) || (a == (1+1)^-1 *: (b+c))).
proof: Proof. rewrite /cong !congP_aux' /sqr_L2_norm_1D neq_mx eqf_sqr. rewrite -subr_eq0 opprB addrBDB subr_eq0. rewrite -[(b 0 0 - a 0 0 == a 0 0 - c 0 0)]subr_eq0. rewrite opprB addrACA -[X in _ + X]opprB opprK. rewrite subr_eq0 -[a 0 0]mul1r -mulrDl. apply /orP/orP. move=> [/eqP H|/eqP H]; [left|right]. apply /eqP /matrixP=> i j. by rewrite !ord1 H. apply /eqP /matrixP=> i j. by rewrite !ord1 !mxE H mulKf ?add11_neq0. move=> [/eqP->|/eqP->]; [left|right]; rewrite ?eqxx //. by rewrite !mxE /= mulrA divff ?add11_neq0 ?mul1r. 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