proposition: Lemma five_segment_aux3 a b c d l mu: (#c) == (1-l) *: #a + l *: (#b) -> mu == l * Num.sqrt(omd b b/ omd a a) -> mu != 0 -> (omd a d/ omd c d) ^+2 = (mu^+2 * (((1-l)/mu)^+2 + (1-l) / mu * 2%:R * Num.sqrt(dist a d/ dist b d) + dist a d/dist b d))^-1.
proof: Proof. move=> /eqP c_eq /eqP mu_eq mu_neq0. apply /eqP. rewrite eq_sym invf_eq ?expr2 ?mulf_eq0 ?invr_eq0 ?omd_eq0 //. rewrite -!expr2 invrK eq_sym -exprVn invf_div. have: omd c d == (1-l) * omd a d + l * (omd b d). rewrite /omd c_eq /omd_v mulmxDl dotC mxE dotC -scalemxAl. rewrite -scalemxAl opprD [(l *: (_*m (_)^T)) 0 0]mxE. rewrite addrA eq_sym mulrBr mulrBr !mulr1. by rewrite addrCA !addrA [l + 1 - l]addrAC subrr add0r !mxE eqxx. move=> /eqP ->. rewrite [(_ + _)/omd a d]mulrDl -[X in (X+_)^+2]mulrA. rewrite divff ?omd_eq0 // mulr1 expr2 mulrDl mulrDr -expr2. rewrite mulrDr -expr2 -[l* omd _ _ / omd _ _]mulrA exprMn. rewrite [X in _ + _ + (X + _)]mulrC eq_sym. rewrite ![mu^+2 * (_ +_)]mulrDr exprMn exprVn mulrCA. rewrite divff; last by rewrite expr2 mulf_neq0. rewrite mulrA mulrA mulrCA {1}[mu^+2]expr2 -[mu*(mu)/mu]mulrA. rewrite divff // !mulr1 mulrAC mu_eq mulrA mulrA mulrA. rewrite -[_ * _* Num.sqrt _ *Num.sqrt _]mulrA -sqrtrM ?mulr_ge0 ?invr_ge0 ?omd_ge0 //. rewrite exprMn sqr_sqrtr ?mulr_ge0 ?invr_ge0 ?omd_ge0 //. rewrite -[X in _+ _+X]mulrA -[X in _+ _+X]mulrA. have: omd b b / omd a a * (dist a d / dist b d) == (omd b d / omd a d)^+2. rewrite /dist/dist_v -!/(omd _ _). rewrite invf_div !mulrA [omd b b / omd a a * omd a a]mulrAC. rewrite -[omd b b * omd a a / omd a a]mulrA divff ?omd_eq0 //. rewrite !invfM !mulrA -mulrAC mulrC !mulrA [(omd b b)^-1 * omd b b]mulrC. rewrite divff ?omd_eq0 // !mul1r mulrC !mulrA [_^-1 *_]mulrC. rewrite divff ?omd_eq0 // mul1r -invfM -expr2. by rewrite -mulrA -expr2 mulrC exprMn exprVn. move=> /eqP ->. rewrite sqrtr_sqr ger0_norm ?mulr_ge0 ?invr_ge0 ?omd_ge0 //. by rewrite /GRing.natmul /= mulrDr !mulr1 !mulrA !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