proposition: Lemma upper_dim a b c p q : p <> q -> a <> b -> a <> c -> b <> c -> cong a p a q -> cong b p b q -> cong c p c q -> (bet a b c \/ bet b c a \/ bet c a b).
proof: Proof. move=> ? _ _ _ H1 H2 H3; apply col_2D. move: (cong_perp H1) (cong_perp H2) (cong_perp H3); set m := (1 / (1 + 1)) *: (p + q). move=> HP1 HP2 HP3; move: (upper_dim_aux HP2 HP1) (upper_dim_aux HP3 HP2). rewrite opprB; set mp0 := p 0 0 - m 0 0; set pm1 := m 0 1 - p 0 1. set ba0 := a 0 0 - b 0 0; set ba1 := a 0 1 - b 0 1; set cb0 := b 0 0 - c 0 0; set cb1 := b 0 1 - c 0 1; move=> E1 E2. have: (mp0 * pm1 * (ba0 * cb1) == mp0 * pm1 * (ba1 * cb0)). by apply /eqP; rewrite mulrACA E1 -E2 -mulrACA [pm1* mp0]mulrC. rewrite -subr_eq0 -mulrBr mulf_eq0 subr_eq0 mulf_eq0=> /orP[/orP[C1|C2]|->//]; by [apply upper_dim_dgc1 with p q|apply upper_dim_dgc2 with p q]. 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