proposition: Lemma Bounded_T_twice_pos: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->(-1<=x<=1)%R->(-1<=y<=1)%R->(0<(e*y*r+f*y+g*r+h)*(e*x*r+f*x+g*r+h))%R.
proof: Proof. intros a b c d e f g h r x y H_vanish Hr Hx Hy; destruct (Qtrichotomy_inf Zero h) as [[Hh|Hh]|Hh]. apply Rlt_mult_pos_pos; apply Bounded_T_pos with a b c d; trivial. apply False_ind; apply (Bounded_T_nonzero a b c d e f g h); auto. apply Rlt_mult_neg_neg; apply Bounded_T_neg with a b c d; trivial. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs