proposition: Lemma segment_construction_aux3 a b c d : (omd a b ^+ 2 - omd b b/dist c d * omd a a)/(omd a a * omd b b) = 1/dist a b - 1 / dist c d.
proof: Proof. rewrite mulrBl -[_^+2/_]invrK invf_div. rewrite /omd -/(dist_v _ _) -/(dist _ _) -!/(omd _ _). rewrite [(omd a a *_)^-1]invfM mulrA -[_/_*_/_]mulrA. rewrite divff ?omd_eq0 // !mul1r mulr1. by rewrite mulrAC divff ?omd_eq0 // mul1r. 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