proposition: Lemma dist_eq1' a b: dist a b == 1 -> (a=b).
proof: Proof. move=> dist_ab. apply /eqP. move: dist_ab. rewrite /dist /dist_v -!/(omd _ _). rewrite divf_eq1 ?expr2 ?mulf_neq0 ?omd_eq0 //. rewrite -expr2. case: (((#a)*m(#b)^T) 0 0 =P norm(#a) * norm(#b)). rewrite /omd/omd_v point_vector_eq => pab_eq. case: (#b =P 0). move ->. rewrite [#a*m 0^T]dotC !mul0mx [X in _*(1 - X)]mxE [X in (1-X)^+2]mxE /=. rewrite subr0 expr2 !mulr1 subr_eq -subr_eq0 opprD. rewrite addrA subrr sub0r oppr_eq0. by rewrite quad_eq0'. move=> /eqP b_neq0 H. suffices: (norm(#a) - norm(#b))^+2 == 0. rewrite sqrf_eq0 subr_eq0 /norm eqr_sqrt ?quad_ge0 // => /eqP na_nb_eq. have: (# a *m (# b)^T) 0 0 == `|(# a *m (# b)^T) 0 0|. rewrite eq_sym -ger0_def. by rewrite pab_eq mulr_ge0 ?norm_ge0. move=> /eqP pab_abs. assert (pab_eq2 := pab_eq). move/eqP: pab_eq. rewrite pab_abs cauchy_schwartz_eq' //. move => /eqP ->. rewrite pab_eq2. have: norm(#a) == norm(#b) by rewrite /norm eqr_sqrt ?quad_ge0 ?na_nb_eq. move => /eqP ->. rewrite /norm -sqrtrM -?expr2 ?quad_ge0 //. rewrite sqrtr_sqr. have: `|(# b *m (# b)^T) 0 0| == (# b *m (# b)^T) 0 0. by rewrite -ger0_def quad_ge0. move=> /eqP ->. by rewrite divff ?scale1r ?quad_neq0. rewrite -cong_identity_aux. by rewrite subr_eq0 eq_sym !norm_sqr -pab_eq H. rewrite -divf_eq1 ; last by rewrite expr2 mulf_eq0 omd_eq0. move=> /eqP pab_neq /eqP dist_eq1. exfalso. suffices: 1 < (1-(norm(#a))^+2) * (1-(norm(#b))^+2)/(1-norm(#a) * norm(#b))^+2. rewrite -invf_lt1; last by rewrite ?mulr_gt0 -?exprVn ?exprn_gt0 ?invr_gt0 ?subr_gt0 ?expr2 ?mulr_ilt1 ?norm_ge0 ?norm_point_lt1. rewrite invf_div divf_lt1; last by rewrite mulr_gt0 ?subr_gt0 ?expr2 ?mulr_ilt1 ?norm_ge0 ?norm_point_lt1. rewrite -subr_lt0 cong_identity_aux. move=> H_lt0. suffices: (norm(#a) - norm(#b))^+2 < 0 <= (norm(#a) - norm(#b))^+2. by rewrite lt_le_asym. by rewrite H_lt0 sqr_ge0. rewrite -[X in X < _]dist_eq1. rewrite !norm_sqr -!/(omd_v _ _) -!/(omd _ _). have : (omd a b)^-1 < (1 - norm (# a) * norm (# b))^-1. rewrite invf_lt_invf ?subr_gt0 ?mulr_ilt1 ?norm_ge0 ?norm_point_lt1 ?p_scalar_point_lt1 //. rewrite /omd /omd_v -subr_gt0 opprB !addrA addrC !addrA [-1+1]addrC. rewrite subrr sub0r addrC subr_gt0 lt_def. rewrite eq_sym pab_neq. by move:(cauchy_schwartz' (#a) (#b))=> /andP[_ ->]. move=> ?. rewrite -subr_gt0 -mulrBr ?mulr_gt0 ?omd_gt0 //. by rewrite subr_gt0 -!exprVn !expr2 ltr_pmul ?invr_ge0 ?omd_ge0. 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