proposition: Lemma upper_dim_aux_2 (a p q : @Point R 1) (k := Num.sqrt(omd p p/ omd q q)) : cong' a p a q -> (omd a p /omd a q == k).
proof: Proof. rewrite /cong'/cong_v=> cong_apaq . have: omd a p ^+ 2 / (omd a a * omd p p) * (omd a a * omd p p)/omd a q ^+ 2 == omd a q ^+ 2 / (omd a a * omd q q) * (omd a a * omd p p)/omd a q ^+ 2 by rewrite -subr_eq0 -mulrBl -mulrBl !mulf_eq0 !omd_eq0 invr_eq0 sqrf_eq0 omd_eq0 !orbF subr_eq0 cong_apaq. set t_ap := omd a p. set t_aq := omd a q. set t_aa := omd a a. set t_pp := omd p p. set t_qq := omd q q. rewrite -[ (_ *_) *(_* _)]mulrA [((t_aa * t_pp)^-1*(t_aa*t_pp))]mulrC. rewrite divff ?mulf_neq0 ?omd_eq0//. rewrite eq_sym mulrC !mulrA expr2. rewrite -[(t_aq * t_aq)^-1 * t_aq * t_aq ]mulrC mulrA. rewrite -[t_aq/(t_aq*t_aq)*t_aq]mulrC mulrA divff ?mulf_neq0 ?omd_eq0 //. rewrite mul1r invfM mulrC !mulrA mulrAC mulrC !mulrA mulrAC. rewrite -!mulrA divff ?omd_eq0 //. rewrite mulr1 eq_sym !mulrA mulr1 -!expr2 /k. rewrite -eqr_sqrt ?mulr_ge0 ?invr_ge0 ?expr2 ?mulr_ge0 ?omd_ge0 //. rewrite [X in _ == Num.sqrt(X)]mulrC => /eqP <-. rewrite sqrtrM ?mulr_ge0 ?omd_ge0 //. rewrite -!expr2 -exprVn !sqrtr_sqr !ger0_norm ?omd_ge0 //. by rewrite invr_ge0 omd_ge0. 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