proposition: Lemma upper_dim_dgc2_aux (a p q : 'rV[R]_2) (m := (1 / (1 + 1)) *: (p + q)) : m 0 1 - p 0 1 = 0 -> m 0 0 - p 0 0 != 0 -> cong a p a q -> m 0 0 = a 0 0.
proof: Proof. move=> E NE /congP/eqP C; move: C; 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 E. rewrite subr0 addr0 addrC [X in _ == X]addrC add2r_eq sqrrB [X in _ == X]sqrrD. rewrite -!addrA add2r_eq !addrA -subr_eq -addrA subrr addr0 -mulr2n eq_sym. rewrite -subr_eq0 -mulNrn -mulNr opprB -mulNrn -mulNr opprB -mulrnDr mulrn_eq0. rewrite mulf_eq0 /= subr_eq0 => /orP [/eqP->//|/eqP H]. by move: NE; rewrite H eqxx. 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