proposition: Lemma cong_perp (a p q : 'rV[R]_2) (m := (1 / (1 + 1)) *: (p + q)) : cong a p a q -> (p 0 0 - m 0 0) * (m 0 0 - a 0 0) + (p 0 1 - m 0 1) * (m 0 1 - a 0 1) = 0.
proof: Proof. move=> /congP/eqP E; move: E; rewrite /sqr_L2_norm_2D. rewrite -(cong_perp_aux1 a p m) -[p 0 1 - a 0 1](cong_perp_aux1 a p m). rewrite -(cong_perp_aux2 a p q) -[q 0 1 - a 0 1](cong_perp_aux2 a p) -!/m. rewrite -[p 0 0 - m 0 0]opprB; set x0 := m 0 0 - a 0 0; set y0 := m 0 0 - p 0 0. rewrite -[p 0 1 - m 0 1]opprB; set x1 := m 0 1 - a 0 1; set y1 := m 0 1 - p 0 1. rewrite !mulNr -subr_eq eq_sym -addrA [X in _ == X]addrC -subr_eq !subr_sqr. rewrite eq_sym -opprB mulNr -sub0r subr_eq eq_sym !addrDBB [X in _ * X]addrC. rewrite !addrBDD !mulrnAl !mulrnAr -!mulrnA -mulrnDl mulrn_eq0 muln_eq0 /=. by rewrite addr_eq0=> /eqP E; rewrite -E addrC subrr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec