proposition: Lemma Incl_M_R_unfolded:forall mu r, (-1<=r<=1)%R->Incl_M mu RR -> (0<=as_Moebius mu r<=1)%R.
proof: Proof. intros ((a,b),(c,d)) r H_r; unfold as_Moebius, Incl_M, map_digits, fst, snd; intros [H_vanish [H1 [H2 [H3 H4]]]]; generalize (Bounded_M_d_minus_c_nonzero _ _ _ _ H_vanish); intro H_cd1; generalize (Bounded_M_c_plus_d_nonzero _ _ _ _ H_vanish); intro H_cd2; assert (Hdc:d + c <> Zero);[ring_exact_Q H_cd2|]. destruct (Qle_dec_weak Zero (a*d-b*c)) as [H_det|H_det]; split. apply Rle_trans with ((b-a)/(d-c))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_5; trivial. stepl ((a*(-1)+b)/(c*(-1)+d))%R. apply (det_nonneg_nondecreasing _ _ _ _ (-1)%R r H_vanish H_det min_one_is_in_base_interval H_r (proj1 H_r)). apply (f_equal2 Rdiv); ring... apply Rle_trans with ((a+b)/(c+d))%R. stepr ((a*1+b)/(c*1+d))%R. apply (det_nonneg_nondecreasing _ _ _ _ r (1)%R H_vanish H_det H_r one_is_in_base_interval (proj2 H_r)). apply (f_equal2 Rdiv); ring. rationalify_R; apply Incl_M_R_unfolded_auxiliary_6; trivial... apply Rle_trans with ((a+b)/(c+d))%R. rationalify_R; apply Incl_M_R_unfolded_auxiliary_7; trivial. stepl ((a*1+b)/(c*1+d))%R. apply (det_nonpos_nonincreasing _ _ _ _ r (1)%R H_vanish H_det H_r one_is_in_base_interval (proj2 H_r)). apply (f_equal2 Rdiv); ring... apply Rle_trans with ((b-a)/(d-c))%R. stepr ((a*(-1)+b)/(c*(-1)+d))%R. apply (det_nonpos_nonincreasing _ _ _ _ (-1)%R r H_vanish H_det min_one_is_in_base_interval H_r (proj1 H_r)). apply (f_equal2 Rdiv); ring. rationalify_R; apply Incl_M_R_unfolded_auxiliary_8; trivial. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Bounded_M