proposition: Lemma segment_construction_aux5 a b c d: ((dist a b)^-1 - omd a b / omd a a + omd b b / omd a a - omd a b / omd a a + (dist c d)^-1 * (omd a b / omd a a - 1 + omd a b / omd a a - omd b b / omd a a)) * ((dist a b)^-1 - (dist c d)^-1) = (dist a b)^-2 + dist c d ^-2 * ( 1 - 2%:R * omd a b/omd a a) - 2%:R/dist a b * omd a b / omd a a + 2%:R/dist c d * (omd a b/ omd a a) - 2%:R/dist c d/dist a b * (1 - omd a b /omd a a) + (dist a b)^-1 * omd b b /omd a a - (dist c d)^-1 * ((dist a b) ^-1 * omd b b /omd a a) + (dist c d)^-2 * (omd b b/ omd a a) - (dist c d)^-1 * (omd b b/ omd a a).
proof: Proof. apply /eqP. rewrite eq_sym /GRing.natmul /=. rewrite ![(1+1)*_]mulrDl ![(1*_+_)*_]mulrDl ![(1*_*_+_)*_]mulrDl. rewrite !opprD !mul1r !addrA. rewrite -[_- (dist a b)^-1 * omd a b / omd a a + (dist c d)^-1 * (omd a b / omd a a)]addrA. rewrite [- ((dist a b)^-1 * omd a b / omd a a) + (dist c d)^-1 * (omd a b / omd a a)]addrC. rewrite -[_*omd a b/omd a a]mulrA -mulrBl. rewrite -[_ + (dist c d)^-1 * (omd a b / omd a a)]addrAC. rewrite -[_ + (dist c d)^-1 * (omd a b / omd a a)]addrAC. rewrite -[_ + (dist c d)^-1 * (omd a b / omd a a) - _]addrA. rewrite -mulrBl. rewrite ![_+ dist c d ^-2 *(omd b b / omd a a)]addrAC. rewrite -[_+_+dist c d^-2 * _]addrA -mulrDr. rewrite addrAC !addrA -[_-(dist c d)^-1*(omd b b/omd a a)]addrA. rewrite -[_ * omd b b/ omd a a]mulrA -mulrBl. rewrite -[((dist c d)^-1 - (dist a b)^-1)]opprB mulNr. rewrite [_+((dist a b)^-1 - (dist c d)^-1) * _]addrAC. rewrite [_+((dist a b)^-1 - (dist c d)^-1) * _]addrAC. rewrite [_+((dist a b)^-1 - (dist c d)^-1) * _]addrAC. rewrite [_+((dist a b)^-1 - (dist c d)^-1) * _]addrAC. rewrite -[_-((dist a b)^-1 - (dist c d)^-1) * _]addrA. rewrite -mulrBr. rewrite -[X in _+_+X+_+_+_+_]mulrN. rewrite -[_+((dist a b)^-1 - (dist c d)^-1) * _]addrA. rewrite -mulrDr. rewrite {1}[(dist c d)^-1 / dist a b * _]mulrDr mulr1. rewrite opprD !addrA ![_-(dist c d)^-1 / dist a b]addrAC. rewrite -exprVn expr2 -mulrBl. rewrite ![_+((dist a b)^-1 - (dist c d)^-1)*_]addrAC. rewrite -mulrDr !addrA. rewrite [X in _-X==_]mulrA -addrA. rewrite -![- ((dist c d)^-1 / dist a b * _)]mulrN. rewrite -mulrDr -addrA -mulrDr !opprD !opprK !addrA. rewrite -[dist c d ^- 2 *_]opprK -[-(dist c d ^- 2 *_)]mulrN. rewrite !opprB opprD !addrA addrAC. rewrite [(_-_)-1]addrAC [(_+_)-1]addrAC. rewrite -exprVn expr2 [(dist c d)^-1 / dist a b]mulrC. by rewrite -mulrA -mulrA -addrA -mulrBl -mulrDr mulrC. 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