proposition: Lemma det_nonneg_refining_endpoints:forall a b c d, Is_refining_M ((a,b),(c,d)) -> Zero <= a*d-b*c -> as_Moebius_Q ((a,b),(c,d)) (-Qone)<=as_Moebius_Q ((a,b),(c,d)) Qone.
proof: Proof. intros a b c d [H_bounded _] H_det. unfold as_Moebius_Q; simpl. assert (H : (-1 <= 1)%R) by fourier. generalize (det_nonneg_nondecreasing _ _ _ _ (-1) 1 H_bounded H_det min_one_is_in_base_interval one_is_in_base_interval H). let t_local:= (destruct H_bounded as [[H1 H2]|[H1 H2]]; simpl in H1, H2; auto) in rationalify_R_goal; [ intro H_Rle; apply Q_to_R_Qle; assumption | stepl (d-c); try ring; t_local | stepl (d+c); try ring;t_local ]. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M