proposition: Lemma dist'_ge0 a b : 0 <= omd a b ^+ 2 - omd a a * omd b b.
proof: Proof. apply le_trans with ((1-norm(#a) * norm(#b))^+2 - (1-(norm(#a))^+2) * (1-(norm(#b))^+2)). by rewrite cong_identity_aux sqr_ge0. rewrite !norm_sqr -!/(omd_v _ _) -!/(omd _ _). rewrite ler_sub ?lexx //. move: (cauchy_schwartz' (#a) (#b)) => /andP [_ ?]. by rewrite expr2 ler_pmul ?subr_ge0 ?mulr_ile1 ?norm_ge0 ?norm_point_le1 //; rewrite /omd/omd_v ler_sub ?lexx. 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