proposition: Lemma cong_identity_aux v w: (1-norm(v) * norm w)^+2 - (1-(norm(v))^+2) * (1-(norm(w))^+2) = (norm(v) - norm(w))^+2 .
proof: Proof. apply /eqP. rewrite -subr_eq0 ![(_-_)^+2]expr2. rewrite !mulrBl !mulrBr !mul1r !mulr1 !opprD !opprK !addrA. rewrite mulrA -mulrAC [_*_*_*_]mulrC !mulrA ![norm w * norm v]mulrC. rewrite -expr2 -mulrA -expr2. set n_v2 := norm v^+2. set n_w2 := norm w^+2. set n_vw := norm v * norm w. rewrite [1 - n_vw - n_vw + n_v2 * n_w2 - 1]addrC. rewrite !addrA [-1+1]addrC subrr add0r. rewrite [- n_vw - n_vw + n_v2 * n_w2 + n_w2 + n_v2 - n_v2 * n_w2 - n_v2 + n_vw]addrC. rewrite !addrA subrr add0r. rewrite [- n_vw + n_v2 * n_w2 + n_w2 + n_v2 - n_v2 * n_w2 - n_v2 + n_vw ]addrC. rewrite !addrA subrr add0r. rewrite [n_v2 * n_w2 + n_w2 + n_v2 - n_v2 * n_w2]addrC. rewrite !addrA [- (n_v2 * n_w2) + n_v2 * n_w2 ]addrC subrr add0r. by rewrite -addrC !addrA -addrA subrr addr0 addrC subrr. 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 algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence