proposition: Lemma as_Moebius_L_one: as_Moebius LL (1)%R = (0)%R.
proof: Proof. unfold as_Moebius, map_digits, fst, snd; realify_Q; auto; simpl; replace (2+1) with 3; [|ring]; replace (1 / 2 * 1 + 3 / 2) with 2; field; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M