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