proposition: Lemma Bounded_M_twice_pos:forall a b c d x y, Bounded_M ((a,b),(c,d))->(-1<=x<=1)%R->(-1<=y<=1)%R-> (0<(c*y+d)*(c*x+d))%R.
proof: Proof. intros a b c d x y H_vanish Hx Hy. destruct (Qtrichotomy_inf Zero d) as [[Hd|Hd]|Hd]. apply Rlt_mult_pos_pos; apply Bounded_M_pos with a b; trivial. apply False_ind; apply (Bounded_M_nonzero a b c d); auto. apply Rlt_mult_neg_neg; apply Bounded_M_neg with a b; trivial. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs