proposition: Lemma segment_construction_aux1 a b c d : 2%:R * ((omd b b/dist c d) * (((#a)*m(#b)^T) 0 0 - norm (# a) ^+ 2) + omd a b * (((#a)*m(#b)^T) 0 0 - norm (# b) ^+ 2)) /2%:R / (omd a a * omd b b) = 1/dist c d * (1 - omd a b/ omd a a) + omd a b/ omd a a - 1/dist a b.
proof: Proof. apply /eqP. rewrite [2%:R*_/_]mulrAC divff ?lt0r_neq0 ?ltr0n //. rewrite !mul1r !norm_sqr !seg_aux7 mulrBr. rewrite [omd b b /dist c d]mulrC. rewrite -![(dist c d)^-1 * _ * _]mulrA. rewrite -mulrBr [omd a b * ( _ -_)]mulrBr. rewrite mulrDl mulrBl -expr2 -[_^+2/_]invrK. rewrite [(_^+2/_)^-1]invf_div /omd -/(dist_v _ _). rewrite -!/(omd _ _) -/(dist _ _). rewrite -mulrA mulrBl [omd b b * _]mulrC divff ?mulf_neq0 ?omd_eq0 //. rewrite mulrAC [_ * omd b b]mulrC [(omd b b * _)^-1]invfM. rewrite mulrA divff ?omd_eq0 // mul1r mulrC. rewrite mulrA -[_*_/omd b b]mulrA divff ?omd_eq0 //. by rewrite mulr1 addrA 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