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