proposition: Lemma as_Moebius_endpoints_digits_base_r: forall d:Digit, (as_Moebius d 1%R<=1)%R.
proof: Proof. intros [ | | ]; [ rewrite as_Moebius_L_one | rewrite as_Moebius_R_one | rewrite as_Moebius_M_one ]; fourier. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M