proposition: Lemma bet_dist_bet' a b c : bet' a b c -> bet_dist a b c.
proof: Proof. rewrite /bet_dist /bet_dist_v. move=>/orP[|betS_abc]. by move=>/betEP[[-> <-]|->|->] ; rewrite -!/(dist _ _); rewrite dist_aa_eq1 subrr sqrtr0 ?mulr0 ?mul0r addr0 expr1n invr1 ?mulr1 ?mul1r. rewrite /dist_v -!/(omd _ _) -subr_eq0. rewrite -!mulrA -mulrBr mulf_eq0 omd_eq0 orFb. rewrite [X in _ - X]mulrC -!mulrA. rewrite [X in _ - X]mulrC -!mulrA. rewrite [X in _ - X]mulrC -!mulrA. rewrite -mulrBr mulf_eq0 omd_eq0 orFb. rewrite subr_eq0 !mulrA mulrAC mulrC -!mulrA -expr2. rewrite -!exprVn -!exprMn eqf_sqr. suffices: ((omd a c)^-1 == ((omd a b)^-1 * ((omd b c)^-1 * ((1 + Num.sqrt (1 - omd a a * (omd b b * (omd a b)^-1 ^+ 2)) * Num.sqrt (1 - omd b b * (omd c c * (omd b c)^-1 ^+ 2)))^-1 * omd b b)))) = true. by move->. apply /eqP /eqP. rewrite !exprVn. rewrite invf_eq ; last by rewrite ?mulf_neq0 ?invr_eq0 ?omd_eq0 ?lt0r_neq0 ?addr_ge_gt0 ?ltr01 ?mulr_ge0 ?sqrtr_ge0. rewrite !invfM !invrK. rewrite !mulrA mulrDr mulr1. rewrite eq_sym -divf_eq1 ?omd_eq0 //. rewrite -!mulrA -!invfM divf_eq1 ?mulf_neq0 ?omd_eq0 //. rewrite -subr_eq0 addrAC addr_eq0. move: betS_abc=> /betSP[bet_eq betR_gt0 betR_lt1]. move/eqP: bet_eq. rewrite eq_sym scalerBr -subr_eq0. rewrite -addrA addr_eq0 opprD !opprK. have: (betR (#a) (#b) (#c))^-1 != 0 by rewrite lt0r_neq0 ?invr_gt0. move=> l_neq0. rewrite (scaler_eq _ _ l_neq0). rewrite scalerDr !scalerA mulrC divff ?lt0r_neq0 // !scale1r. rewrite scalerBr [_ - _]addrC addrA -{1}[#a]scale1r -scalerBl. move: l_neq0 ; set l := (betR (#a) (#b) (#c))^-1 => l_neq0 /eqP c_eq. have: (omd a b * omd b c - omd b b * omd a c == (1 - l) * (omd a b ^+ 2 - omd a a * omd b b)). rewrite ![omd _ c]omd_reflexivity. rewrite ![omd c _]/omd/omd_v c_eq. rewrite omd_cb omd_ca. rewrite [omd _ _ * (_ + _)]mulrDr [omd _ _ * (_ + _)]mulrDr. rewrite opprD addrAC !addrA -addrA addrC. rewrite [- (omd b b * (l * omd a b)) + omd a b * (l * omd b b)]addrC. rewrite mulrCA [X in _- X]mulrC mulrA subrr add0r. rewrite mulrCA -expr2 [X in _ -X]mulrCA -mulrBr. by rewrite [omd b b * _]mulrC eqxx. move /eqP ->. rewrite eq_sym mulrA mulrACA. rewrite -{1}[omd a b]ger0_norm ?omd_ge0 //. rewrite -{1}[omd b c]ger0_norm ?omd_ge0 //. rewrite -!sqrtr_sqr. rewrite -sqrtrM; last by rewrite expr2 mulr_ge0 ?omd_ge0. rewrite -sqrtrM; last by rewrite expr2 mulr_ge0 ?omd_ge0. rewrite ![_^+2 * (_ - _)]mulrBr !mulr1. rewrite [_^+2 * (_)]mulrC. rewrite [_^+2 * (_)]mulrC. rewrite -!expr2 !mulrA -!mulrA -!expr2. rewrite ![_^-2 * _^+2]mulrC ?divff ?expr2 ?mulf_neq0 ?omd_eq0 //. rewrite !mulr1 -sqrtrM -!expr2 ?dist'_ge0 //. have: (omd b c ^+ 2 - omd b b * omd c c) == ((1-l)^+2 * (omd a b ^+ 2 - omd a a * omd b b)). rewrite [omd b c]omd_reflexivity. 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 ->. rewrite [omd c b]/omd/omd_v c_eq omd_cb. rewrite sqrrD !exprMn. rewrite [omd b b * _]mulrDr [omd b b * _]mulrDr [omd b b * _]mulrDr. rewrite !opprD. rewrite [-(omd b b * ((1 - l) ^+ 2 * omd a a)) - omd b b * (l ^+ 2 * omd b b)]addrC. rewrite !addrA -!addrA addrC !addrA -!addrA addrC. rewrite !addrA -!addrA addrC !addrA. rewrite [omd b b * (l ^+ 2 * omd b b)]mulrC expr2 expr2 mulrA. rewrite subrr sub0r addrC !addrA -!addrA. rewrite addrCA !addrA -!addrA addrC !addrA. rewrite mulrAC [ omd b b * ((1 - l) * l * omd a b)]mulrC. rewrite -mulrA -[(1 - l) * l * omd a b * omd b b]mulrA. rewrite [omd a b * omd b b]mulrC mulrA mulrA mulrA. rewrite subrr sub0r addrAC addrC !addrA subrr add0r. rewrite [X in _ - X]mulrC. by rewrite -[X in _ - X]mulrA -mulrBr eqxx. move /eqP ->. rewrite mulrCA -expr2 -exprMn sqrtr_sqr. rewrite ler0_norm ; last rewrite nmulr_rle0 ?subr_lt0 ?invf_gt1 ?dist'_ge0 //. by rewrite opprK 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