proposition: Lemma det_nonpos_nonincreasing:forall a b c d x y, Bounded_M ((a,b),(c,d)) -> a*d-b*c <= Zero -> (-1<=x<=1)%R -> (-1<=y<=1)%R -> (x<=y)%R -> ((a*y+b)/(c*y+d)<=(a*x+b)/(c*x+d))%R.
proof: Proof. intros a b c d x y H_vanish H_det Hx Hy Hxy; generalize (Bounded_M_nonzero_denum _ _ _ _ _ H_vanish Hx); generalize (Bounded_M_nonzero_denum _ _ _ _ _ H_vanish Hy); generalize (Bounded_M_twice_pos _ _ _ _ _ _ H_vanish Hy Hx); generalize (Q_to_Rle _ _ H_det); rewrite Q_to_R_Zero; rewrite Q_to_Rminus; repeat rewrite Q_to_Rmult; clear H_det; intros H_det H_cxyd H_cyd H_cxd; apply Rle_zero_Rminus; rewrite (distance_Moebius a b _ _ _ _ H_cxd H_cyd); unfold Rdiv; apply Fourier_util.Rle_mult_inv_pos; auto; apply Rle_mult_nonpos_nonpos; trivial; apply Rle_minus; trivial. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs