proposition: Lemma five_segment_aux4 a b : omd a a / omd a b = Num.sqrt(omd a a * dist a b/ omd b b).
proof: Proof. apply /eqP. rewrite /dist/dist_v -!/(omd _ _) eq_sym !mulrA mulrAC. rewrite mulrC !mulrA -mulrA divff ?omd_eq0 //. rewrite mulr1 mulrC mulrCA -expr2 mulrC -exprVn -exprMn. by rewrite sqrtr_sqr ger0_norm ?mulr_ge0 ?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