proposition: Lemma upper_dim : upper_dimP (@Point R 1) (@bet' R 1) (@cong' R 1).
proof: Proof. move => a b c p q /eqP neq_pq _ _ _ H1 H2 H3. suffices: (((#a 0 0) - (#b 0 0)) * ((#b 0 1) - (#c 0 1))) == (((#a 0 1) - (#b 0 1)) * ((#b 0 0) - (#c 0 0))). rewrite /bet'; apply col_2D. set (k := Num.sqrt(omd p p/ omd q q)). set (e := #p-k*:#q). suffices: ( ((#a 0 0 * e 0 0 + #a 0 1 * e 0 1) == (#b 0 0 * e 0 0 + #b 0 1 * e 0 1)) && ((#b 0 0 * e 0 0 + #b 0 1 * e 0 1) == (#c 0 0 * e 0 0 + #c 0 1 * e 0 1))). case: (e 0 1 =P 0) ; case: (e 0 0 =P 0). move => E00 E01 _. suffices: (#p == #q). rewrite -point_vector_eq=> pq_eq //. exfalso. move/negP: neq_pq. by rewrite pq_eq. have: (e == 0) by rewrite vector2_eq E00 E01 !mxE /= eqxx. rewrite /e subr_eq0 => /eqP p_eqkq. suffices: k = 1. by rewrite p_eqkq=>->; rewrite scale1r eqxx. have:(k = Num.sqrt ((1 - ((k*k) *: (# q *m (# q)^T)) 0 0) / (1 - (# q *m (# q)^T) 0 0))). by rewrite {1}/k /omd/omd_v p_eqkq -scalemxAl dotC -scalemxAl scalerA. move=>H. have: ( 0 < k) by rewrite sqrtr_gt0 mulr_gt0 ?invr_gt0 ?omd_gt0. move=> k_gt0. have: k^+2 == 1. move: (eqf_sqr k (Num.sqrt ((1 - ((k * k) *: (# q *m (# q)^T)) 0 0) / (1 - (# q *m (# q)^T) 0 0)))). rewrite {4}H eqxx /= [X in _ == X]sqr_sqrtr. move => /eqP P1. have: k ^+ 2 * (1 - (# q *m (# q)^T) 0 0) == (1 - ((k * k) *: (# q *m (# q)^T)) 0 0). rewrite P1 mulrAC -mulrA divff ?lt0r_neq0 ?subr_gt0 // ; last by destruct q. by rewrite mulr1 eqxx. rewrite mulrBr mulr1 subr_eq expr2 addrAC -addrA. by rewrite !mxE /= subrr addr0. by rewrite le0r -sqrtr_gt0 -H k_gt0 orbT. by rewrite sqrp_eq1 ?le0r ?k_gt0 ?orbT // => /eqP ->. move=> /eqP /negPf NX0 ->. rewrite !mulr0 !addr0 -subr_eq0 -[X in _ && X]subr_eq0 -!mulrBl. rewrite !mulf_eq0 NX0 !Bool.orb_false_r !subr_eq0=> /andP[/eqP -> /eqP ->]. by rewrite !subrr mulr0 mul0r eqxx. move=> -> /eqP /negPf NX0. rewrite !mulr0 !add0r -subr_eq0 -[X in _ && X]subr_eq0 -!mulrBl. rewrite !mulf_eq0 NX0 !Bool.orb_false_r !subr_eq0 => /andP[/eqP -> /eqP ->]. by rewrite !subrr mulr0 mul0r eqxx. move=> /eqP /negPf NX0 /eqP /negPf NX1. rewrite -subr_eq0 opprD addrCA -[_-_]addrA -mulrBl addrCA addrA -mulrBl -[X in _ + X]opprK subr_eq0. rewrite Bool.andb_comm. rewrite -subr_eq0 opprD addrCA -[_-_]addrA -mulrBl addrCA addrA -mulrBl -[X in _ + X]opprK subr_eq0. move=> /andP[/eqP H4 /eqP H5]. suffices: (# a 0 0 - # b 0 0) * e 0 0 * -(# b 0 1 - # c 0 1) * e 0 1 == (# b 0 0 - # c 0 0) * e 0 0 * -(# a 0 1 - # b 0 1) * e 0 1. rewrite -subr_eq0 -mulrBl mulf_eq0. rewrite mulrC [X in _ - X]mulrC !mulrA -mulrBl mulf_eq0. move: NX0 NX1 => -> ->. rewrite subr_eq0 mulrC [X in _ == X]mulrC !mulrN eqr_opp [X in _ == X]mulrC. rewrite !Bool.orb_false_r. exact. move: H4 H5 => -> ->. rewrite -mulrA mulrC !mulrN !mulNr mulrA. by rewrite eqxx. move: (upper_dim_aux H1) (upper_dim_aux H2) (upper_dim_aux H3). move => -> -> ->. by rewrite eqxx. 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