proposition: Lemma segment_construction_aux6 a b: (dist a b)^-1 * omd b b / omd a a = (omd a b/omd a a)^+2.
proof: Proof. rewrite /dist/dist_v -!/(omd _ _) invf_div invfM. rewrite mulrA -[X in X / omd a a]mulrA [_^-1*_]mulrC. rewrite divff ?omd_eq0 // mulr1 -mulrA -invfM -expr2. by rewrite -exprVn -exprMn. 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