proposition: Lemma five_segment_aux5 a b c l: (#c) == (1-l) *: #a + l *: (#b) -> l != 0 -> a!=b-> a!=c-> (omd a c/l/omd a b)^+2 = (1 - dist a b)/(1- dist a c).
proof: Proof. move=> /eqP c_eq l_neq0 ab_neq bc_neq. apply /eqP. rewrite -divf_eq1; last by rewrite mulf_neq0 ?invr_eq0 ?subr_eq0 1?eq_sym ?dist_neq1. rewrite invf_div mulrA divf_eq1 ; last by rewrite subr_eq0 eq_sym dist_neq1. rewrite mulrDr mulr1 mulrN /(dist a c)/dist_v -!/(omd _ _). rewrite -{2}mulrA [(omd a c * _)^+2]exprMn mulrA. rewrite [X in _ -X]mulrAC [X in _ -X*_]mulrAC divff; last by rewrite expr2 mulf_eq0 omd_eq0. rewrite omd_reflexivity {1}/omd/omd_v c_eq omd_ca. rewrite mulrDl [l * omd a b / l]mulrAC divff //. rewrite mulrDl mul1r divff ?omd_eq0 //. rewrite sqrrD [1^+2]expr2 !mul1r !mulr1. rewrite addrC !addrA mulrC -[(1 - l) * omd a a / l / omd a b]mulrA. rewrite [(_*(l^-1 / omd a b))^+2]exprMn -mulNr. rewrite -mulrDl /(omd c c)/omd_v c_eq omd_cc. rewrite mulrDr mulrDr [omd a a * ((1 - l) ^+ 2 * omd a a)]mulrCA. rewrite -expr2 -exprMn !opprD [_ + _^+2] addrC addrA. rewrite addrA subrr sub0r -opprD mulNr. rewrite [(_)*(l^-1/omd a b)^+2]mulrDl exprMn !exprVn. rewrite mulrA mulrAC mulrA -[omd a a * l ^+ 2 / l ^+ 2]mulrA. rewrite divff; last by rewrite expr2 mulf_neq0 ?l_neq0. rewrite mulr1 mulrAC {1}/omd {1}/omd {1}/omd. rewrite -/(dist_v _ _) -/(dist _ _). rewrite [X in dist a b + X]mulrA [l * (1 - l) * omd a b *+ 2]addrC. rewrite mulrDr [X in dist a b + X/_]mulrDl [X in dist a b + X]mulrDl. rewrite mulrA mulrAC mulrC [omd a b ^+2]expr2. rewrite invfM invfM mulrA mulrA mulrA mulrA mulrC mulrA. rewrite mulrA mulrA -mulrA divff ?omd_eq0 // mulr1. rewrite mulrACA mulrA mulrC mulrA mulrA mulrA mulrC. rewrite mulrA mulrA mulrA mulrA -mulrA divff ?l_neq0 //. rewrite mulr1 mulrC mulrA mulrA mulrAC mulrC mulrA mulrA. rewrite !opprD addrA -[-_-_-_+_]addrA [X in -_-_+X]addrC. rewrite subrr addr0 addrC addrA addrA -addrA [X in 1 -_+X]addrC. by rewrite subrr addr0 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