proposition: Lemma Bounded_M_d_minus_c_nonzero: forall a b c d, Bounded_M ((a,b),(c,d)) -> d-c<> Zero.
proof: Proof. intros a b c d [[H1 H2]|[H1 H2]]; unfold fst, snd in H1; unfold fst, snd in H2; auto; apply sym_not_eq; auto. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs