proposition: Lemma distance_Moebius:forall a b c d x y, c*y+d<>0 -> c*x+d<>0 -> ((a*y+b)/(c*y+d))-((a*x+b)/(c*x+d))=((y-x)*(a*d-b*c))/((c*y+d)*(c*x+d)).
proof: Proof. intros a b c d x y Hcyd Hcxd; rewrite Rminus_Rdiv; auto; apply (f_equal2 Rdiv); ring. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier