proposition: Lemma det2_nonneg_nondecreasing:forall a b c d e f g h r x y, Bounded_T (((a,b),(c,d)),((e,f),(g,h))) -> (-1<=r<=1)%R -> (0 <= (a*r+b)*(g*r+h)-(c*r+d)*(e*r+f))%R -> (-1<=x<=1)%R -> (-1<=y<=1)%R -> (x<=y)%R -> ((a*x*r+b*x+c*r+d)/(e*x*r+f*x+g*r+h)<=(a*y*r+b*y+c*r+d)/(e*y*r+f*y+g*r+h))%R.
proof: Proof. intros a b c d e f g h r x y H_vanish Hr H_det Hx Hy Hxy; generalize (Bounded_T_nonzero_denum _ _ _ _ _ _ _ _ _ _ H_vanish Hy Hr); generalize (Bounded_T_nonzero_denum _ _ _ _ _ _ _ _ _ _ H_vanish Hx Hr); generalize (Bounded_T_twice_pos _ _ _ _ _ _ _ _ _ _ _ H_vanish Hr Hx Hy); intros H_cxyr H_rx H_ry; apply Rle_zero_Rminus; rewrite (distance_Tensor a b c d _ _ _ _ _ _ _ H_ry H_rx); unfold Rdiv; apply Fourier_util.Rle_mult_inv_pos; auto; apply Rmult_le_pos; trivial; apply Rle_Rminus_zero; trivial. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs