proposition: Lemma upper_dim_aux (a p q : @Point R 1) (k := Num.sqrt(omd p p/ omd q q)) (e := #p-k*:#q) : cong' a p a q -> #a 0 0 * e 0 0 + #a 0 1 * e 0 1 = (1-k).
proof: Proof. move=> cong_apaq. apply upper_dim_aux_2 in cong_apaq. suffices: omd a p == k * omd a q ; [move => H1|]. suffices: (#a *m e^T) 0 0 == 1 - k ; [move => /eqP <-|]. rewrite !mxE !big_ord_recr /= big_ord0 add0r !mxE. congr (# a 0 _ * (# p 0 _ - k * # q 0 _) + # a 0 _ * (# p 0 _ - k * # q 0 _)) ; by apply: val_inj. rewrite /e dotC mulmxBl mxE eq_sym subr_eq addrC addrA addrC addrA -subr_eq. move/eqP: H1. rewrite /omd/omd_v dotC => ->. rewrite mulrBr mulr1 -subr_eq0 opprD addrA addrC. rewrite !addrA [- k + k]addrC subrr add0r -scalemxAl. by rewrite dotC !mxE /= subrr eqxx. move/eqP: cong_apaq. rewrite /e /k=> <-. by rewrite mulrAC -mulrA divff ?mulr1 ?eqxx ?omd_eq0. 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