proposition: Lemma upper_dim : upper_dimP Point bet' cong'.
proof: Proof. move=> a b c p q ? _ _ _ H1 H2 H3; apply col_2D_bet'. 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 choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra) mathcomp(zmodp) GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence