proposition: Lemma Bounded_T_nonzero_denum:forall a b c d e f g h x y, Bounded_T (((a,b),(c,d)),((e,f),(g,h))) -> (-1<=x<=1)%R->(-1<=y<=1)%R->(e*x*y+f*x+g*y+h<>0)%R.
proof: Proof. intros a b c d e f g h x y H_vanish Hx Hy; destruct (Qtrichotomy_inf Zero h) as [[Hh|Hh]|Hh]; [ apply Rlt_not_eq'; apply Bounded_T_pos with a b c d; trivial | intros _; apply (Bounded_T_nonzero a b c d e f g h); auto | apply Rlt_not_eq; apply Bounded_T_neg with a b c d; trivial]. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs