proposition: Lemma Bounded_M_nonzero: forall a b c d, Bounded_M ((a,b),(c,d)) -> d<> Zero.
proof: Proof. intros a b c d [[H1 H2]|[H1 H2]] H3; unfold fst, snd in H1; unfold fst, snd in H2; generalize H1 H2; clear H1 H2; rewrite H3; unfold Qminus; repeat rewrite Qplus_zero_left; intros H1 H2; apply Qlt_irreflexive with Zero; apply Qlt_transitive with c; trivial; apply Qlt_opp; [ stepl Zero | stepr Zero]; trivial; ring. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs