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