proposition: Lemma poly_cong a b c d r (K := omd b b / dist c d): ((norm (# b) ^+ 2 - ((#a)*m(#b)^T) 0 0) ^+ 2 +K * norm (# a - # b) ^+ 2) * r ^+ 2 + 2%:R * (K * (((#a)*m(#b)^T) 0 0 - norm (# a) ^+ 2) + omd a b * (((#a)*m(#b)^T) 0 0 - norm (# b) ^+ 2)) *r + (omd a b ^+ 2 - K * omd a a) == 0 -> cong_v (#b) (extension (#a) (#b) r^-1) (#c) (#d).
proof: Proof. set E := (extension (#a) (#b) r^-1). have : 2%:R == (1+1 ) :> R. by rewrite /GRing.natmul /=. move=> /eqP rew2. have : ((norm (# b) ^+ 2 - (# a *m (# b)^T) 0 0) ^+ 2 + K * norm (# a - # b) ^+ 2) * r ^+ 2 + 2%:R * (K * ((# a *m (# b)^T) 0 0 - norm (# a) ^+ 2) + omd a b * ((# a *m (# b)^T) 0 0 - norm (# b) ^+ 2)) * r + (omd a b ^+ 2 - K * omd a a) == (omd_v (#b) E)^+2 - K * (1-norm(E)^+2). rewrite eq_sym /omd_v. have : norm(E)^+2 == norm(#a)^+2 + r^+2 * norm(#b-#a)^+2 + r * (2%:R *( (#a*m(#b)^T) 0 0-norm(#a)^+2)). rewrite /E /extension invrK norm_sqr mulmxDl. rewrite ![_*m(r*:_+_)^T]dotC !mulmxDl. rewrite -!scalemxAl ![_*m(r*:(_-_))^T]dotC -!scalemxAl scalerA. rewrite [(# b - # a) *m (# a)^T]mulmxDl mulNmx. rewrite !addrA mxE mxE mxE mxE -norm_sqr -expr2 mxE mxE. rewrite [(- (# a *m (# a)^T)) 0 0]mxE -norm_sqr addrC !addrA -addrA. rewrite -mulrDr [(#b)*m(#a)^T]dotC. by rewrite /GRing.natmul /= mulrDl mul1r !addrA eqxx. move=> /eqP ->. rewrite {1}/E /extension invrK dotC [X in X *m _^T]addrC. rewrite mulmxDl -scalemxAl mulmxDl mxE [X in (1 -(_ + X))^+ 2]mxE. rewrite [(# b *m (# b)^T + - # a *m (# b)^T) 0 0]mxE. rewrite -norm_sqr opprD addrA -/(omd_v _ _) -/(omd _ _). rewrite mulNmx mxE. rewrite !opprD addrA addrA addrA [norm(#a)^+2]norm_sqr. rewrite -/(omd_v (#a) (#a)) -/(omd _ _) -norm_sqr. rewrite sqrrB exprMn [K *(_)]mulrBr [K *(_)]mulrBr. rewrite !opprD !addrA !opprK addrC. rewrite !addrA addrAC addrC [K * (r ^+ 2 *_)]mulrC. rewrite -[r ^+ 2 * _ * K]mulrA !addrA -addrA -mulrDr. rewrite [omd a b * (r * (_ - _))]mulrC. rewrite addrC !addrA -addrA -opprD. rewrite -[r*(norm(#b)^+2-_)]mul1r -!mulrDl -rew2. rewrite addrAC addrC !addrA -addrA. rewrite [K * (r * (2%:R * ((_-_^+ 2))))]mulrCA. rewrite [2%:R * ( r * _)]mulrCA [r * (2%:R * _)]mulrA. rewrite -[r * 2%:R * _ * _]mulrA -[r * 2%:R * _ ]mulrA -mulrBr. rewrite [K * (2%:R * _)]mulrCA -mulrBr. rewrite addrAC -addrA -addrA addrC !addrA. rewrite -addrA [- (K * omd a a) + omd a b ^+ 2]addrC addrA. rewrite [r^+2 *_]mulrC [norm (# b - # a) ^+ 2 * K]mulrC. have : norm(#b - #a)^+2 == norm(#a - #b)^+2. rewrite !norm_sqr !mulmxBl ![_*m(_+_)^T]dotC !mulmxBl. rewrite [#b*m(#a)^T]dotC !opprB !addrA. rewrite -addrA addrACA [#b*m(#b)^T+# a *m (# a)^T]addrC. by rewrite addrACA !addrA eqxx. move=> /eqP ->. rewrite [r * (2%:R * _)]mulrC -[-(_*omd a b)]mulNr. by rewrite opprB [(_*omd a b)]mulrC eqxx. move=> /eqP ->. case:(norm(E)^+2 =P 1). move=> /eqP. rewrite sqr_norm_eq1 ger0_norm ?norm_ge0 // => /eqP normE_eq1. rewrite normE_eq1 [1^+2]expr2 mulr1 subrr mulr0 subr0 sqrf_eq0 => omdBE_eq0. exfalso. suffices: 0 < omd_v (#b) E by rewrite lt_def omdBE_eq0. rewrite /omd_v subr_gt0. apply le_lt_trans with (norm(#b) * norm(E)). by move: (cauchy_schwartz' (#b) E) => /andP[_ ->]. by rewrite normE_eq1 mulr1 norm_point_lt1. move=> /eqP normE_neq1. rewrite subr_eq0 -divf_eq1; last by rewrite mulf_neq0 ?subr_eq0 ?lt0r_neq0 /K ?mulr_gt0 ?invr_gt0 ?omd_gt0 ?dist_gt0 // eq_sym. rewrite /cong_v -[_==(_/_)]divf_eq1; last by rewrite invfM ?mulf_neq0 ?invr_neq0 -/(omd _ _) ?omd_eq0. rewrite norm_sqr -/(omd_v _ _) => H. rewrite invf_div -/(dist_v _ _) -/(dist _ _). rewrite -!/(omd _ _) -[dist c d]invrK -mulrA -invfM. by rewrite [omd b b * _ /_]mulrAC -/K. 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