proposition: Lemma segment_construction_aux2 a b c d : ((norm (# b) ^+ 2 - ((#a)*m(#b)^T) 0 0) ^+ 2 + omd b b/dist c d* norm (# a - # b) ^+ 2) /(omd a a * omd b b) = 1/dist a b - omd a b / omd a a + omd b b / omd a a - omd a b / omd a a + 1/dist c d * (omd a b / omd a a - 1 + omd a b / omd a a - omd b b / omd a a).
proof: Proof. rewrite norm_sqr seg_aux7 sqrrB /GRing.natmul /= seg_aux8. rewrite !mul1r [omd b b/_]mulrC -[_*_*_]mulrA. rewrite [omd b b * _]mulrBr. rewrite [omd b b * _]mulrDr. rewrite [omd b b * _]mulrBr. rewrite mulrDl mulrDl mulrBl -[_^+2/_]invrK invf_div. rewrite /omd -/(dist_v _ _) -/(dist _ _) -!/(omd _ _). rewrite mulrDl [omd a a * omd b b]mulrC. rewrite [(omd b b*_)^-1]invfM expr2 mulrA mulrA. rewrite -![_*_*(omd b b)^-1]mulrA divff ?omd_eq0 //. rewrite !mulr1 -mulrA [_*(_/_)]mulrBl [_*(_/_)]mulrDl. rewrite [_*(_/_)]mulrBl ![_*omd a _]mulrC !mulrA. rewrite -![_*_*(omd b b)^-1]mulrA divff ?omd_eq0 //. rewrite !mulr1 divff ?omd_eq0 //. by rewrite opprD addrA [_ - _ -_ +_]addrAC. 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