proposition: Lemma Is_refining_T_denom_nonvanishing_T:forall xi r1 r2, Is_refining_T xi -> ((-1)<=r1<=1)%R ->((-1)<=r2<=1)%R -> denom_nonvanishing_T xi r1 r2.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) r1 r2 H_refining H_r1 H_r2; generalize (Is_refining_T_h_minusplus_efg_sign_dec _ _ _ _ _ _ _ _ H_refining); generalize H_refining; clear H_refining; intros [H_bounded _] [[_[_[_[_[_[_[_[_[H1 [H2 [H3 [H4 H5]]]]]]]]]]]]|[_[_[_[_[_[_[_[_[H1 [H2 [H3 [H4 H5]]]]]]]]]]]]]; red; simpl. apply Rlt_not_eq'; apply (Bounded_T_pos _ _ _ _ _ _ _ _ _ _ H_bounded H5 H_r1 H_r2). apply Rlt_not_eq; apply (Bounded_T_neg _ _ _ _ _ _ _ _ _ _ H_bounded H5 H_r1 H_r2). Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier