proposition: Lemma as_Moebius_endpoints_digits_base_l: forall d:Digit, ((-1)%R<=as_Moebius d (-1)%R)%R.
proof: Proof. intros [ | | ]; [ rewrite as_Moebius_L_min_one | rewrite as_Moebius_R_min_one | rewrite as_Moebius_M_min_one ]; fourier. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M