proposition: Lemma Bounded_T_pos:forall a b c d e f g h x y, Bounded_T (((a,b),(c,d)),((e,f),(g,h))) -> Zero<h ->(-1<=x<=1)%R->(-1<=y<=1)%R->(0<e*x*y+f*x+g*y+h)%R.
proof: Proof. intros a b c d e f g h x y H_vanish; generalize (Bounded_T_M_1 _ _ _ _ _ _ _ _ H_vanish); generalize (Bounded_T_M_2' _ _ _ _ _ _ _ _ H_vanish); generalize H_vanish; intros [[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]] H_vanish2 H_vanish1 Hh Hx Hy; unfold fst, snd in H1; unfold fst, snd in H2; unfold fst, snd in H3; unfold fst, snd in H4; (stepr ((e*y+f)*x+ (g*y+h))%R; [|ring]). assert (H_hf1:Zero<h-f); [apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((e-f-g+h)+(-e-f+g+h)); auto; ring|]. assert (H_hf2:Zero<h+f); [apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((e+f+g+h)+(-e+f-g+h)); auto; ring|]. assert (H_hg1:Zero<h-g); [apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((e-f-g+h)+(-e+f-g+h)); auto; ring|]. assert (H_hg1_R:(0<h-g)%R); [rewrite <- Q_to_R_Zero; rewrite <- Q_to_Rminus; apply Q_to_Rlt; trivial|]. assert (H_hg2:Zero<h+g); [apply Qlt_Qmult_cancel_l with (Qone+Qone); auto; stepl Zero; auto; stepr ((e+f+g+h)+(-e-f+g+h)); auto; ring|]. assert (H_hg2_R:(0<h+g)%R); [rewrite <- Q_to_R_Zero; rewrite <- Q_to_Rplus; apply Q_to_Rlt; trivial|]. assert (H_h_R:(0<h)%R); [rewrite <- Q_to_R_Zero; apply Q_to_Rlt; trivial|]. destruct (Rtrichotomy_inf 0 (e*y+f)) as [[Hef|Hef]|Hef]. apply Bounded_M_pos_auxiliary_1; trivial; stepr (Qminus g e * y + Qminus h f)%R; [ apply (Bounded_M_pos _ _ _ _ y H_vanish1); trivial | repeat rewrite Q_to_Rminus; ring]... rewrite <- Hef; stepr (g*y+h)%R; [|ring]. destruct (Qtrichotomy_inf Zero g) as [[Hg|Hg]|Hg]. generalize (Q_to_Rlt _ _ Hg); clear Hg; rewrite Q_to_R_Zero; intro Hg; apply Bounded_M_pos_auxiliary_1; trivial... rewrite <- Hg; rewrite Q_to_R_Zero; stepr h; trivial; ring... generalize (Q_to_Rlt _ _ Hg); clear Hg; rewrite Q_to_R_Zero; intro Hg; apply Bounded_M_pos_auxiliary_2; trivial... apply Bounded_M_pos_auxiliary_2; trivial; stepr (Qplus g e * y + Qplus h f)%R; [ apply (Bounded_M_pos _ _ _ _ y H_vanish2); trivial | repeat rewrite Q_to_Rplus; ring]... apply False_ind; apply Qlt_irreflexive with Zero; apply Qlt_transitive with (h+h+h+h); auto; stepl ((e + f + g + h)+(e - f - g + h)+(- e - f + g + h)+(- e + f - g + h)); auto; ring. Qed.
imports: digits Bounded_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs