proposition: Lemma Is_refining_M_L:Is_refining_M (LL:Matrix).
proof: Proof. unfold map_digits, Is_refining_M, Bounded_M, fst, snd; split; left; repeat split; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M