proposition: Lemma Incl_T_R_unfolded:forall xi r1 r2,(-1<=r1<=1)%R->(-1<=r2<=1)%R->Incl_T xi RR -> (0<=as_Tensor xi r1 r2<=1)%R.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) r1 r2 H_r1 H_r2; unfold as_Tensor, Incl_T, map_digits, fst, snd; replace 3%Z with (2+1)%Z; trivial; rewrite (Z_to_Qplus 2 1); intros [H_vanish [H1 [H2 [H3 [H4 [H5 [H6 [H7 H8]]]]]]]]; generalize (Bounded_T_e_mf_mg_h_nonzero _ _ _ _ _ _ _ _ H_vanish); generalize (Bounded_T_me_mf_g_h_nonzero _ _ _ _ _ _ _ _ H_vanish); generalize (Bounded_T_me_f_mg_h_nonzero _ _ _ _ _ _ _ _ H_vanish); generalize (Bounded_T_e_f_g_h_nonzero _ _ _ _ _ _ _ _ H_vanish); intros H_efgh4 H_efgh3 H_efgh2 H_efgh1; generalize (Bounded_T_M_1 _ _ _ _ _ _ _ _ H_vanish); generalize (Bounded_T_M_2 _ _ _ _ _ _ _ _ H_vanish); intros H_vanish2 H_vanish1. destruct (Rle_dec_weak 0 ((a*r2+b)*(g*r2+h)-(c*r2+d)*(e*r2+f))) as [H_det2|H_det2]; split. apply Rle_trans with (((Qminus c a)*r2+(Qminus d b))/((Qminus g e)*r2+(Qminus h f)))%R. destruct (Qle_dec_weak 0 ((c-a)*(h-f)-(d-b)*(g-e))) as [H_det|H_det]. apply Rle_trans with (((a-c)+(d-b))/((e-g)+(h-f)))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_7; trivial. ring_exact_Q H_efgh1. ring_exact_Q H1... stepl (((Qminus c a)*(-1)+(Qminus d b))/((Qminus g e)*(-1)+(Qminus h f)))%R. apply (det_nonneg_nondecreasing (c-a) (d-b) (g-e) (h-f) (-1)%R r2 H_vanish1 H_det min_one_is_in_base_interval H_r2 (proj1 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((c-a)+(d-b))/((g-e)+(h-f)))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_7; trivial. ring_exact_Q H_efgh2. ring_exact_Q H3... stepl (((Qminus c a)*1+(Qminus d b))/((Qminus g e)*1+(Qminus h f)))%R. apply (det_nonpos_nonincreasing (c-a) (d-b) (g-e) (h-f) r2 (1)%R H_vanish1 H_det H_r2 one_is_in_base_interval (proj2 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... stepl ((a*(-1)*r2+b*(-1)+c*r2+d)/(e*(-1)*r2+f*(-1)+g*r2+h))%R. apply (det2_nonneg_nondecreasing _ _ _ _ _ _ _ _ _ _ _ H_vanish H_r2 H_det2 min_one_is_in_base_interval H_r1 (proj1 H_r1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((Qplus a c)*r2+(Qplus b d))/((Qplus e g)*r2+(Qplus f h)))%R. stepr ((a*1*r2+b*1+c*r2+d)/(e*1*r2+f*1+g*r2+h))%R. apply (det2_nonneg_nondecreasing _ _ _ _ _ _ _ _ _ _ _ H_vanish H_r2 H_det2 H_r1 one_is_in_base_interval (proj2 H_r1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... destruct (Qle_dec_weak 0 ((a+c)*(f+h)-(b+d)*(e+g))) as [H_det|H_det]. apply Rle_trans with (((a+c)+(b+d))/((e+g)+(f+h)))%R. stepr (((Qplus a c)*1+(Qplus b d))/((Qplus e g)*(1)+(Qplus f h)))%R. apply (det_nonneg_nondecreasing (a+c) (b+d) (e+g) (f+h) r2 (1)%R H_vanish2 H_det H_r2 one_is_in_base_interval (proj2 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; apply Incl_M_R_unfolded_auxiliary_6; trivial. ring_exact_Q H_efgh4. ring_exact_Q H8... apply Rle_trans with (((b+d)-(a+c))/((f+h)-(e+g)))%R. stepr (((Qplus a c)*(-1)+(Qplus b d))/((Qplus e g)*(-1)+(Qplus f h)))%R. apply (det_nonpos_nonincreasing (a+c) (b+d) (e+g) (f+h) (-1)%R r2 H_vanish2 H_det min_one_is_in_base_interval H_r2 (proj1 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; apply Incl_M_R_unfolded_auxiliary_8; trivial. ring_exact_Q H6... apply Rle_trans with (((Qplus a c)*r2+(Qplus b d))/((Qplus e g)*r2+(Qplus f h)))%R. destruct (Qle_dec_weak 0 ((a+c)*(f+h)-(b+d)*(e+g))) as [H_det|H_det]. apply Rle_trans with (((b+d)-(a+c))/((f+h)-(e+g)))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_5; trivial. ring_exact_Q H5... stepl (((Qplus a c)*(-1)+(Qplus b d))/((Qplus e g)*(-1)+(Qplus f h)))%R. apply (det_nonneg_nondecreasing (a+c) (b+d) (e+g) (f+h) (-1)%R r2 H_vanish2 H_det min_one_is_in_base_interval H_r2 (proj1 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((a+c)+(b+d))/((e+g)+(f+h)))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_7; trivial. ring_exact_Q H_efgh4. ring_exact_Q H7... stepl (((Qplus a c)*1+(Qplus b d))/((Qplus e g)*(1)+(Qplus f h)))%R. apply (det_nonpos_nonincreasing (a+c) (b+d) (e+g) (f+h) r2 (1)%R H_vanish2 H_det H_r2 one_is_in_base_interval (proj2 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... stepl ((a*1*r2+b*1+c*r2+d)/(e*1*r2+f*1+g*r2+h))%R. apply (det2_nonpos_nonincreasing _ _ _ _ _ _ _ _ _ _ _ H_vanish H_r2 H_det2 H_r1 one_is_in_base_interval (proj2 H_r1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... apply Rle_trans with (((Qminus c a)*r2+(Qminus d b))/((Qminus g e)*r2+(Qminus h f)))%R. stepr ((a*(-1)*r2+b*(-1)+c*r2+d)/(e*(-1)*r2+f*(-1)+g*r2+h))%R. apply (det2_nonpos_nonincreasing _ _ _ _ _ _ _ _ _ _ _ H_vanish H_r2 H_det2 min_one_is_in_base_interval H_r1 (proj1 H_r1)). realify_Q_goal; apply (f_equal2 Rdiv); ring... destruct (Qle_dec_weak 0 ((c-a)*(h-f)-(d-b)*(g-e))) as [H_det|H_det]. apply Rle_trans with (((c-a)+(d-b))/((g-e)+(h-f)))%R. stepr (((Qminus c a)*1+(Qminus d b))/((Qminus g e)*1+(Qminus h f)))%R. apply (det_nonneg_nondecreasing (c-a) (d-b) (g-e) (h-f) r2 (1)%R H_vanish1 H_det H_r2 one_is_in_base_interval (proj2 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; apply Incl_M_R_unfolded_auxiliary_6; trivial. ring_exact_Q H_efgh2. ring_exact_Q H4... apply Rle_trans with (((a-c)+(d-b))/((e-g)+(h-f)))%R. stepr (((Qminus c a)*(-1)+(Qminus d b))/((Qminus g e)*(-1)+(Qminus h f)))%R. apply (det_nonpos_nonincreasing (c-a) (d-b) (g-e) (h-f) (-1)%R r2 H_vanish1 H_det min_one_is_in_base_interval H_r2 (proj1 H_r2)). realify_Q_goal; apply (f_equal2 Rdiv); ring... rationalify_R; apply Incl_M_R_unfolded_auxiliary_6; trivial. ring_exact_Q H_efgh1. ring_exact_Q H2... Qed.
imports: digits Bounded_M Bounded_T Incl_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs